Removing a source of clash with multiple recursive patterns in notations.

The same variable name was used to collect the binders and the
successive steps of matching one binder, resulting in unexpected
attempts for merging in the presence of multiple occurrence of the
same recursive pattern.

An amusing side-effect: when eta-expanding for a notation with
recursive binders, it is the second variable of the "x .. y" which is
used to invent a name rather than the first one.

3 files changed, 45 insertions, 45 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1fcb49af2..fb1baae0a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -631,7 +631,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
     match c with
     | NVar id when Id.equal id ldots_var -> Option.get terminopt
     | NVar id -> subst_var subst' (renaming, env) id
-    | NList (x,_,iter,terminator,lassoc) ->
+    | NList (x,y,iter,terminator,lassoc) ->
       let l,(scopt,subscopes) =
         (* All elements of the list are in scopes (scopt,subscopes) *)
         try
@@ -646,7 +646,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
           anomaly (Pp.str "Inconsistent substitution of recursive notation") in
       let termin = aux (terms,None,None) subinfos terminator in
       let fold a t =
-        let nterms = Id.Map.add x (a, (scopt, subscopes)) terms in
+        let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in
         aux (nterms,None,Some t) subinfos iter
       in
       List.fold_right fold l termin
@@ -684,7 +684,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         Some arg
       in
       GHole (loc, knd, naming, arg)
-    | NBinderList (x,_,iter,terminator) ->
+    | NBinderList (x,y,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (bl,(scopt,subscopes)) = Id.Map.find x binders in
@@ -692,7 +692,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
 	let letins,bl = subordinate_letins intern [] bl in
         let termin = aux (terms,None,None) (renaming,env) terminator in
 	let res = List.fold_left (fun t binder ->
-	    aux (terms,Some(x,binder),Some t) subinfos iter)
+	    aux (terms,Some(y,binder),Some t) subinfos iter)
 	  termin bl in
 	make_letins letins res
       with Not_found ->
@@ -1349,7 +1349,7 @@ let drop_notations_pattern looked_for =
       RCPatCstr (loc, g,
 		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
 		 List.map (in_pat false scopes) args, [])
-    | NList (x,_,iter,terminator,lassoc) ->
+    | NList (x,y,iter,terminator,lassoc) ->
       if not (List.is_empty args) then user_err_loc
         (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns.");
       (try
@@ -1357,7 +1357,7 @@ let drop_notations_pattern looked_for =
 	 let (l,(scopt,subscopes)) = Id.Map.find x substlist in
          let termin = in_not top loc scopes fullsubst [] terminator in
 	 List.fold_right (fun a t ->
-           let nsubst = Id.Map.add x (a, (scopt, subscopes)) subst in
+           let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in
            let u = in_not false loc scopes (nsubst, substlist) [] iter in
            subst_pat_iterator ldots_var t u)
            (if lassoc then List.rev l else l) termin
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 27aed9d33..e6b5dc50b 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -294,14 +294,14 @@ let compare_recursive_parts found f 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
-	  else iterator) in
+	  f' (if lassoc then iterator
+	      else subst_glob_vars [x,GVar(Loc.ghost,y)] 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' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
 	(* found have been collected by compare_constr *)
 	found := newfound;
 	NBinderList (x,y,iterator,f (Option.get !terminator))
@@ -875,49 +875,48 @@ let remove_sigma x (terms,onlybinders,termlists,binderlists) =
 let remove_bindinglist_sigma x (terms,onlybinders,termlists,binderlists) =
   (terms,onlybinders,termlists,Id.List.remove_assoc x binderlists)
 
-let protecting x f (terms,onlybinders,termlists,binderlists as sigma) =
-  try
-    let previous = Id.List.assoc x binderlists in
-    let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc x binderlists) in
-    let (terms,onlybinders,termlists,binderlists) = f sigma in
-    (terms,onlybinders,termlists,(x,previous)::binderlists)
-  with Not_found ->
-    f sigma
-
 let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
 
-let match_abinderlist_with_app match_fun alp metas sigma rest x iter termin =
+let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
+
+let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin =
   let rec aux sigma bl rest =
     try
-      let (terms,_,_,binderlists as sigma) = match_fun alp (add_ldots_var metas) sigma rest iter in
+      let metas = add_ldots_var (add_meta_bindinglist y metas) in
+      let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in
       let rest = Id.List.assoc ldots_var terms in
       let b =
-        match Id.List.assoc x binderlists with [b] -> b | _ ->assert false
+        match Id.List.assoc y binderlists with [b] -> b | _ ->assert false
       in
-      let sigma = remove_bindinglist_sigma x (remove_sigma ldots_var sigma) in
+      let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in
       aux sigma (b::bl) rest
     with No_match when not (List.is_empty bl) ->
-      let alp,sigma = bind_bindinglist_env alp sigma x bl in
-      match_fun alp metas sigma rest termin in
-  protecting x (fun sigma -> aux sigma [] rest) sigma
+      bl, rest, sigma in
+  let bl,rest,sigma = aux sigma [] rest in
+  let alp,sigma = bind_bindinglist_env alp sigma x bl in
+  match_fun alp metas sigma rest termin
+
+let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas
 
-let match_alist match_fun alp metas sigma rest x iter termin lassoc =
+let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
   let rec aux sigma acc rest =
     try
-      let (terms,_,_,_ as sigma) = match_fun (add_ldots_var metas) sigma rest iter in
+      let metas = add_ldots_var (add_meta_term y metas) in
+      let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in
       let rest = Id.List.assoc ldots_var terms in
-      let t = Id.List.assoc x terms in
-      let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
+      let t = Id.List.assoc y terms in
+      let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
       aux sigma (t::acc) rest
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
   let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
+  let l = if lassoc then l else List.rev l in
   if is_bindinglist_meta x metas then
     (* This is a recursive pattern for both bindings and terms; it is *)
     (* registered for binders *)
-    bind_bindinglist_as_term_env alp sigma x (if lassoc then l else List.rev l)
+    bind_bindinglist_as_term_env alp sigma x l
   else
-    bind_termlist_env alp sigma x (if lassoc then l else List.rev l)
+    bind_termlist_env alp sigma x l
 
 let does_not_come_from_already_eta_expanded_var =
   (* This is hack to avoid looping on a rule with rhs of the form *)
@@ -940,8 +939,8 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 r1
 
   (* Matching recursive notations for terms *)
-  | r1, NList (x,_,iter,termin,lassoc) ->
-      match_alist (match_hd u alp) alp metas sigma r1 x iter termin lassoc
+  | r1, NList (x,y,iter,termin,lassoc) ->
+      match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc
 
   (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
   | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])),
@@ -951,7 +950,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
       match_in u alp metas sigma t termin
 
   (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
-  | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)->
+  | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
       let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in
       (* TODO: address the possibility that termin is a Lambda itself *)
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
@@ -964,15 +963,15 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma t termin
 
-  | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin)
+  | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
       when na1 != Anonymous ->
       let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in
       (* TODO: address the possibility that termin is a Prod itself *)
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
   (* Matching recursive notations for binders: general case *)
-  | r, NBinderList (x,_,iter,termin) ->
-      match_abinderlist_with_app (match_hd u) alp metas sigma r x iter termin
+  | r, NBinderList (x,y,iter,termin) ->
+      match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin
 
   (* Matching individual binders as part of a recursive pattern *)
   | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2)
@@ -1137,13 +1136,14 @@ let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
     (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::terms,x,termlists,y
 
-let match_cases_pattern_alist match_fun metas sigma rest x iter termin lassoc =
+let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
   let rec aux sigma acc rest =
     try
-      let (terms,_,_,_ as sigma) = match_fun (add_ldots_var metas) sigma rest iter in
+      let metas = add_ldots_var (add_meta_term y metas) in
+      let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in
       let rest = Id.List.assoc ldots_var terms in
-      let t = Id.List.assoc x terms in
-      let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
+      let t = Id.List.assoc y terms in
+      let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
       aux sigma (t::acc) rest
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
@@ -1166,9 +1166,9 @@ let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 =
       else
 	let l1',more_args = Util.List.chop le2 l1 in
 	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
-  | r1, NList (x,_,iter,termin,lassoc) ->
-      (match_cases_pattern_alist (match_cases_pattern_no_more_args)
-	metas (terms,(),termlists,()) r1 x iter termin lassoc),(0,[])
+  | r1, NList (x,y,iter,termin,lassoc) ->
+      (match_cases_pattern_list (match_cases_pattern_no_more_args)
+	metas (terms,(),termlists,()) r1 x y iter termin lassoc),(0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index d9ce42c60..20101f48e 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -12,7 +12,7 @@ let '(a, _, _) := (2, 3, 4) in a
      : nat
 exists myx y : bool, myx = y
      : Prop
-fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
+fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y
      : (nat -> nat -> Prop) -> nat -> Prop
 ∃ n p : nat, n + p = 0
      : Prop