Fixing a bug of recursive notations introduced in dfdaf4de.

When a proper notation variable occurred only in a recursive pattern
of the notation, the notation was wrongly considered non printable due
(the side effect that function compare_glob_constr and that
mk_glob_constr_eq does not do anymore was indeed done by aux' but
thrown away). This fixes it.

3 files changed, 16 insertions, 9 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 034116731..99e18f09e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -297,28 +297,29 @@ let compare_recursive_parts found f f' (iterator,subc) =
 	user_err ?loc:(subtract_loc loc1 loc2)
           (str "Both ends of the recursive pattern are the same.")
     | Some (x,y,RecursiveTerms lassoc) ->
-        let newfound,x,y,lassoc =
+        let toadd,x,y,lassoc =
           if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) ||
              List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found)
           then
-            !found,x,y,lassoc
+            None,x,y,lassoc
           else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) ||
                   List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found)
           then
-            !found,y,x,not lassoc
+            None,y,x,not lassoc
           else
-            (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
+            Some (x,y),x,y,lassoc in
 	let iterator =
 	  f' (if lassoc then iterator
 	      else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
-	(* found have been collected by compare_constr *)
-	found := newfound;
+	(* found variables have been collected by compare_constr *)
+	found := (List.remove Id.equal y (pi1 !found),
+                  Option.fold_right (fun a l -> a::l) toadd (pi2 !found),
+                  pi3 !found);
 	NList (x,y,iterator,f (Option.get !terminator),lassoc)
     | Some (x,y,RecursiveBinders (t_x,t_y)) ->
-	let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
 	let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
 	(* found have been collected by compare_constr *)
-	found := newfound;
+	found := (List.remove Id.equal y (pi1 !found), pi2 !found, (x,y) :: pi3 !found);
 	check_is_hole x t_x;
 	check_is_hole y t_y;
 	NBinderList (x,y,iterator,f (Option.get !terminator))
@@ -348,7 +349,7 @@ let notation_constr_and_vars_of_glob_constr a =
     | _c ->
 	aux' c
   and aux' x = DAst.with_val (function
-  | GVar id -> add_id found id; NVar id
+  | GVar id -> if not (Id.equal id ldots_var) then add_id found id; NVar id
   | GApp (g,args) -> NApp (aux g, List.map aux args)
   | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
   | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index e5dbfcb4b..65efe228a 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -122,3 +122,5 @@ return (1, 2, 3, 4)
      : nat * nat * nat * nat
 {{ 1 | 1 // 1 }}
      : nat
+!!! _ _ : nat, True
+     : (nat -> Prop) * ((nat -> Prop) * Prop)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index b1015137d..ea372ad1a 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -186,3 +186,7 @@ Check letpair x [1] = {0}; return (1,2,3,4).
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
   (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Check 1+1+1.
+
+(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
+Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
+Check !!! (x y:nat), True.