Merge pull request #1086 from MevenBertrand/correct-noccur

Correct noccur for Template
MetaCoq · Sep 16, 2024 · d4a0fff · d4a0fff
2 parents ac6100e + 4c4fc2a
commit d4a0fff
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