Merge PR #981: Miscellaneous fixes for notations

10 files changed, 69 insertions, 48 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 ->
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 4a103cdd23..37204c2134 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -380,9 +380,9 @@ let tag_var = tag Tag.variable
     match bl with
       | [CLocalAssum (nal,k,t)] ->
         kw n ++ pr_binder false pr_c (nal,k,t)
-      | (CLocalAssum _ | CLocalPattern _) :: _ as bdl ->
+      | (CLocalAssum _ | CLocalPattern _ | CLocalDef _) :: _ as bdl ->
         kw n ++ pr_undelimited_binders sep pr_c bdl
-      | _ -> assert false
+      | [] -> assert false
 
   let pr_binders_gen pr_c sep is_open =
     if is_open then pr_delimited_binders pr_com_at sep pr_c
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 9d106d2dac..7bcd7b041c 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -133,3 +133,5 @@ fun (x : nat) (p : x = x) => match p with
                              | 1 => 1
                              end = p
      : forall x : nat, x = x -> Prop
+bar  0
+     : nat
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index b9985a594f..fe6c05c39e 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -291,3 +291,11 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p.
 Notation "1" := eq_refl.
 Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p.
 
+(* Check bug 5693 *)
+
+Module M.
+Definition A := 0.
+Definition bar (a b : nat) := plus a b.
+Notation "" := A (format "", only printing).
+Check (bar A 0).
+End M.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index e5dbfcb4be..65efe228af 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 b1015137d6..ea372ad1a3 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.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 837f2efd06..4d04f2cf9b 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -142,3 +142,8 @@ Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing).
 Reserved Notation "x === y" (at level 50).
 Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
  where "x === y" := (EQ x y).
+
+(* Check that strictly ident or _ are coerced to a name *)
+
+Fail Check {x@{u},y|x=x}.
+Fail Check {?[n],y|0=0}.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8b042a3ca3..c424b1d501 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -98,8 +98,7 @@ let pr_grammar = function
    quote (except a single quote alone) must be quoted) *)
 
 let parse_format ((loc, str) : lstring) =
-  let str = " "^str in
-  let l = String.length str in
+  let len = String.length str in
   let push_token a = function
     | cur::l -> (a::cur)::l
     | [] -> [[a]] in
@@ -109,16 +108,16 @@ let parse_format ((loc, str) : lstring) =
     | a::(_::_ as l) -> push_token (UnpBox (b,a)) l
     | _ -> user_err Pp.(str "Non terminated box in format.") in
   let close_quotation i =
-    if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ')
+    if i < len && str.[i] == '\'' && (Int.equal (i+1) len || str.[i+1] == ' ')
     then i+1
     else user_err Pp.(str "Incorrectly terminated quoted expression.") in
   let rec spaces n i =
-    if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1)
+    if i < len && str.[i] == ' ' then spaces (n+1) (i+1)
     else n in
   let rec nonspaces quoted n i =
-    if i < String.length str && str.[i] != ' ' then
+    if i < len && str.[i] != ' ' then
       if str.[i] == '\'' && quoted &&
-        (i+1 >= String.length str || str.[i+1] == ' ')
+        (i+1 >= len || str.[i+1] == ' ')
       then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n
       else nonspaces quoted (n+1) (i+1)
     else
@@ -126,26 +125,26 @@ let parse_format ((loc, str) : lstring) =
       else n in
   let rec parse_non_format i =
     let n = nonspaces false 0 i in
-    push_token (UnpTerminal (String.sub str i n)) (parse_token (i+n))
+    push_token (UnpTerminal (String.sub str i n)) (parse_token 1 (i+n))
   and parse_quoted n i =
-    if i < String.length str then match str.[i] with
+    if i < len then match str.[i] with
       (* Parse " // " *)
-      | '/' when i <= String.length str && str.[i+1] == '/' ->
+      | '/' when i <= len && str.[i+1] == '/' ->
           (* We forget the useless n spaces... *)
 	  push_token (UnpCut PpFnl)
-            (parse_token (close_quotation (i+2)))
+            (parse_token 1 (close_quotation (i+2)))
       (* Parse " .. / .. " *)
-      | '/' when i <= String.length str ->
+      | '/' when i <= len ->
 	  let p = spaces 0 (i+1) in
 	  push_token (UnpCut (PpBrk (n,p)))
-            (parse_token (close_quotation (i+p+1)))
+            (parse_token 1 (close_quotation (i+p+1)))
       | c ->
       (* The spaces are real spaces *)
       push_white n (match c with
       | '[' ->
-	  if i <= String.length str then match str.[i+1] with
+	  if i <= len then match str.[i+1] with
 	    (* Parse " [h .. ",  *)
-	    | 'h' when i+1 <= String.length str && str.[i+2] == 'v' ->
+	    | 'h' when i+1 <= len && str.[i+2] == 'v' ->
 		  (parse_box (fun n -> PpHVB n) (i+3))
 		(* Parse " [v .. ",  *)
 	    | 'v' ->
@@ -157,39 +156,39 @@ let parse_format ((loc, str) : lstring) =
 	  else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.")
       (* Parse "]"  *)
       | ']' ->
-	  ([] :: parse_token (close_quotation (i+1)))
+	  ([] :: parse_token 1 (close_quotation (i+1)))
       (* Parse a non formatting token *)
       | c ->
 	  let n = nonspaces true 0 i in
 	  push_token (UnpTerminal (String.sub str (i-1) (n+2)))
-	    (parse_token (close_quotation (i+n))))
+	    (parse_token 1 (close_quotation (i+n))))
     else
       if Int.equal n 0 then []
       else user_err Pp.(str "Ending spaces non part of a format annotation.")
   and parse_box box i =
     let n = spaces 0 i in
-    close_box i (box n) (parse_token (close_quotation (i+n)))
-  and parse_token i =
+    close_box i (box n) (parse_token 1 (close_quotation (i+n)))
+  and parse_token k i =
     let n = spaces 0 i in
     let i = i+n in
-    if i < l then match str.[i] with
+    if i < len then match str.[i] with
       (* Parse a ' *)
-      |	'\'' when i+1 >= String.length str || str.[i+1] == ' ' ->
-	  push_white (n-1) (push_token (UnpTerminal "'") (parse_token (i+1)))
+      |	'\'' when i+1 >= len || str.[i+1] == ' ' ->
+	  push_white (n-k) (push_token (UnpTerminal "'") (parse_token 1 (i+1)))
       (* Parse the beginning of a quoted expression *)
       |	'\'' ->
-          parse_quoted (n-1) (i+1)
+          parse_quoted (n-k) (i+1)
       (* Otherwise *)
       | _ ->
-          push_white (n-1) (parse_non_format i)
+          push_white (n-k) (parse_non_format i)
     else push_white n [[]]
   in
   try
-    if not (String.is_empty str) then match parse_token 0 with
+    if not (String.is_empty str) then match parse_token 0 0 with
       | [l] -> l
       | _ -> user_err Pp.(str "Box closed without being opened in format.")
     else
-      user_err Pp.(str "Empty format.")
+      []
   with reraise ->
     let (e, info) = CErrors.push reraise in
     let info = Option.cata (Loc.add_loc info) info loc in