Fixing a bug in recognizing a recursive pattern of notations

immediately in the scope of another recursive pattern.

3 files changed, 25 insertions, 4 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 80c09745d..4a507b37e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -239,7 +239,7 @@ let check_is_hole id = function GHole _ -> () | t ->
 
 let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
 
-let compare_recursive_parts found f (iterator,subc) =
+let compare_recursive_parts found f f' (iterator,subc) =
   let diff = ref None in
   let terminator = ref None in
   let rec aux c1 c2 = match c1,c2 with
@@ -294,14 +294,14 @@ let compare_recursive_parts found f (iterator,subc) =
           else
             (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
 	let iterator =
-	  f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator
+	  f' (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator
 	  else iterator) in
 	(* found have been collected by compare_constr *)
 	found := newfound;
 	NList (x,y,iterator,f (Option.get !terminator),lassoc)
     | Some (x,y,None) ->
 	let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
-	let iterator = f iterator in
+	let iterator = f' iterator in
 	(* found have been collected by compare_constr *)
 	found := newfound;
 	NBinderList (x,y,iterator,f (Option.get !terminator))
@@ -313,7 +313,7 @@ let notation_constr_and_vars_of_glob_constr a =
   let rec aux c =
     let keepfound = !found in
     (* n^2 complexity but small and done only once per notation *)
-    try compare_recursive_parts found aux' (split_at_recursive_part c)
+    try compare_recursive_parts found aux aux' (split_at_recursive_part c)
     with Not_found ->
     found := keepfound;
     match c with
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 823418cc1..8b3fa3161 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -17,3 +17,11 @@ pair (pair O (S (S O))) (pair (S (S O)) O)
 pair (pair (pair O (S (S O))) (S (S (S (S O)))))
   (pair (S (S (S (S O)))) (pair (S (S O)) O))
      : prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+fun x y : nat => Nat.add x y
+     : forall (_ : nat) (_ : nat), nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index f37772534..d79104204 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -19,3 +19,16 @@ Check (((0,2),4),(0,(2,4))).
 Unset Printing Notations.
 Check <<0,2,4>>.
 Set Printing Notations.
+
+(**********************************************************************)
+(* Check notations with recursive notations both in binders and terms *)
+
+Notation "'ETA' x .. y , f" :=
+  (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+  (at level 200, x binder, y binder).
+Check ETA (x:nat) (y:nat), Nat.add.
+Check ETA (x y:nat), Nat.add.
+Check ETA x y, Nat.add.
+Unset Printing Notations.
+Check ETA (x:nat) (y:nat), Nat.add.
+Set Printing Notations.