Merge PR #981: Miscellaneous fixes for notations

3 files changed, 22 insertions, 21 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 2d0a19b9a6..771c137344 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -320,13 +320,13 @@ let coerce_reference_to_id = function
         (str "This expression should be a simple identifier.")
 
 let coerce_to_id = function
-  | { CAst.v = CRef (Ident (loc,id),_); _ } -> (loc,id)
+  | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,id)
   | { CAst.loc; _ } -> CErrors.user_err ?loc
        ~hdr:"coerce_to_id"
          (str "This expression should be a simple identifier.")
 
 let coerce_to_name = function
-  | { CAst.v = CRef (Ident (loc,id),_) } -> (loc,Name id)
-  | { CAst.loc; CAst.v = CHole (_,_,_) } -> (loc,Anonymous)
+  | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,Name id)
+  | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> (loc,Anonymous)
   | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
                          (str "This expression should be a name.")
diff --git a/interp/notation.ml b/interp/notation.ml
index 176ac3bf68..d3cac1e3e9 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -425,7 +425,7 @@ let warn_notation_overridden =
   CWarnings.create ~name:"notation-overridden" ~category:"parsing"
                    (fun (ntn,which_scope) ->
                     str "Notation" ++ spc () ++ str ntn ++ spc ()
-                    ++ strbrk "was already used" ++ which_scope)
+                    ++ strbrk "was already used" ++ which_scope ++ str ".")
 
 let declare_notation_interpretation ntn scopt pat df ~onlyprint =
   let scope = match scopt with Some s -> s | None -> default_scope in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0341167318..3d48114ec6 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)
@@ -823,7 +824,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
        alp, b :: bl
     | _ -> raise No_match in
     let alp, bl = unify alp bl bl' in
-    let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+    let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
     alp, add_bindinglist_env sigma var bl
   with Not_found ->
     alp, add_bindinglist_env sigma var bl
@@ -909,7 +910,7 @@ let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc
   | GLambda (na,bk,t,b) as b0 ->
     begin match na, DAst.get b with
     | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
-      when islambda && is_gvar p e ->
+      when islambda && is_gvar p e && not (occur_glob_constr p b) ->
       match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
     | _, _ when islambda ->
       match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
@@ -918,7 +919,7 @@ let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc
   | GProd (na,bk,t,b) as b0 ->
     begin match na, DAst.get b with
     | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
-      when not islambda && is_gvar p e ->
+      when not islambda && is_gvar p e && not (occur_glob_constr p b) ->
       match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
     | Name _, _ when not islambda ->
       match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
@@ -991,8 +992,6 @@ let does_not_come_from_already_eta_expanded_var glob =
   (* checked). *)
   match DAst.get glob with GVar _ -> false | _ -> true
 
-let is_var c = match DAst.get c with GVar _ -> true | _ -> false
-
 let rec match_ inner u alp metas sigma a1 a2 =
   let open CAst in
   let loc = a1.loc in
@@ -1009,7 +1008,8 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
     begin match na1, DAst.get b1, iter with
     (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
-    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _) when is_gvar p e ->
+    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _)
+      when is_gvar p e && not (occur_glob_constr p b1) ->
       let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
@@ -1027,7 +1027,8 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
     (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
     begin match na1, DAst.get b1, iter, termin with
-    | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _ when is_gvar p e ->
+    | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _
+      when is_gvar p e && not (occur_glob_constr p b1) ->
       let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
@@ -1049,7 +1050,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) ->
     begin match na1, DAst.get b1, na2 with
     | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
-      when is_var e && is_bindinglist_meta id metas ->
+      when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) ->
       let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in
       match_in u alp metas sigma b1 b2
     | _, _, Name id when is_bindinglist_meta id metas ->