From 4c4fc2a85e26e81025835d7483efa20d1b55c08c Mon Sep 17 00:00:00 2001 From: Meven Date: Thu, 23 May 2024 15:59:38 +0100 Subject: [PATCH] correcting the definition of noccur_between in Template --- template-coq/theories/Ast.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/template-coq/theories/Ast.v b/template-coq/theories/Ast.v index e0cf8a9dc..a890e8572 100644 --- a/template-coq/theories/Ast.v +++ b/template-coq/theories/Ast.v @@ -537,7 +537,7 @@ Notation closed t := (closedn 0 t). Fixpoint noccur_between k n (t : term) : bool := match t with - | tRel i => Nat.ltb i k && Nat.leb (k + n) i + | tRel i => Nat.ltb i k || Nat.leb (k + n) i | tEvar ev args => List.forallb (noccur_between k n) args | tLambda _ T M | tProd _ T M => noccur_between k n T && noccur_between (S k) n M | tApp u v => noccur_between k n u && List.forallb (noccur_between k n) v