Fixing #5161 (case of a notation with unability to detect a recursive binder).

Type annotations in unrelated binders were badly interfering with
detection of recursive binders in notations.

1 files changed, 10 insertions, 6 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ec4b2e938..07f27efb5 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -240,6 +240,10 @@ let check_is_hole id = function GHole _ -> () | t ->
     strbrk "In recursive notation with binders, " ++ pr_id id ++
     strbrk " is expected to come without type.")
 
+type recursive_pattern_kind =
+| RecursiveTerms of bool (* associativity *)
+| RecursiveBinders of glob_constr * glob_constr
+
 let compare_recursive_parts found f (iterator,subc) =
   let diff = ref None in
   let terminator = ref None in
@@ -261,18 +265,16 @@ let compare_recursive_parts found f (iterator,subc) =
       let x,y = if lassoc then y,x else x,y in
       begin match !diff with
       | None ->
-        let () = diff := Some (x, y, Some lassoc) in
+        let () = diff := Some (x, y, RecursiveTerms lassoc) in
         true
       | Some _ -> false
       end
   | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term)
   | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) ->
       (* We found a binding position where it differs *)
-      check_is_hole x t_x;
-      check_is_hole y t_y;
       begin match !diff with
       | None ->
-        let () = diff := Some (x, y, None) in
+        let () = diff := Some (x, y, RecursiveBinders (t_x,t_y)) in
         aux c term
       | Some _ -> false
       end
@@ -286,7 +288,7 @@ let compare_recursive_parts found f (iterator,subc) =
 	(* Here, we would need a loc made of several parts ... *)
 	user_err_loc (subtract_loc loc1 loc2,"",
           str "Both ends of the recursive pattern are the same.")
-    | Some (x,y,Some lassoc) ->
+    | Some (x,y,RecursiveTerms lassoc) ->
 	let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in
 	let iterator =
 	  f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator
@@ -294,11 +296,13 @@ let compare_recursive_parts found f (iterator,subc) =
 	(* found have been collected by compare_constr *)
 	found := newfound;
 	NList (x,y,iterator,f (Option.get !terminator),lassoc)
-    | Some (x,y,None) ->
+    | Some (x,y,RecursiveBinders (t_x,t_y)) ->
 	let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
 	let iterator = f iterator in
 	(* found have been collected by compare_constr *)
 	found := newfound;
+	check_is_hole x t_x;
+	check_is_hole y t_y;
 	NBinderList (x,y,iterator,f (Option.get !terminator))
   else
     raise Not_found