diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index cf0d8bda59af..4d3210529a0e 100644
--- 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
new file mode 100644
index 000000000000..81b8907842a0
--- /dev/null
+++ 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).