Fixes coq#17860: missing check in notations with repeated recursive b…

…inder variable.
herbelin · Jul 15, 2023 · 8c8defc · 8c8defc
1 parent f93c42e
commit 8c8defc
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
@@ -591,13 +591,13 @@ let compare_recursive_parts recvars found f f' (iterator,subc) =
         aux c term
       | Some (x', y', RecursiveBinders revert') ->
         check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert';
-        true
+        aux c term
       | Some (x', y', RecursiveTerms revert') ->
         (* Recursive binders have precedence: they can be coerced to
            terms but not reciprocally *)
         check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert';
         let () = diff := Some (x, y, RecursiveBinders revert) in
-        true
+        aux c term
       end
   | _ ->
       mk_glob_constr_eq aux c1 c2 in

diff --git a/test-suite/bugs/bug_17860.v b/test-suite/bugs/bug_17860.v
@@ -0,0 +1,7 @@
+Axiom Reduction_sum : forall {A}, nat -> nat -> nat -> (nat -> A) -> A.
+#[local] Notation "'einsum_partλ0' s => body"
+  := (fun s => Reduction_sum 0 s 1 (fun s => body))
+       (at level 200, s binder, only parsing).
+#[local] Notation "'einsum_partλ' s1 .. sn => body"
+  := (einsum_partλ0 s1 => .. (einsum_partλ0 sn => body) .. )
+       (at level 200, s1 binder, sn binder, only parsing).