correcting the definition of noccur_between in Template

MetaCoq · May 23, 2024 · dcad89f · dcad89f
1 parent d6e0f45
commit dcad89f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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