Merge PR #13099: Locating pattern identifiers (?id) by default at parsing time and use location in some typing error messages

Reviewed-by: ppedrot

18 files changed, 45 insertions, 43 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index fb5d7cc244..8d0bcd1ee6 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -17,6 +17,11 @@
   was instead intended. If cancelling the breaking role of cuts in the
   box was intended, turn `h n c` into `h c`.
 
+### Grammar entries
+
+- `Prim.pattern_identref` is deprecated, use `Prim.pattern_ident`
+  which now returns a located identifier.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index c98e05370e..d14d156ffc 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -108,7 +108,7 @@ and constr_expr_r =
          * constr_expr * constr_expr
   | CHole   of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
   | CPatVar of Pattern.patvar
-  | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
+  | CEvar   of Glob_term.existential_name CAst.t * (lident * constr_expr) list
   | CSort   of Glob_term.glob_sort
   | CCast   of constr_expr * constr_expr Glob_term.cast_type
   | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index ce8e7d3c2c..7075d082ee 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -156,7 +156,7 @@ let rec constr_expr_eq e1 e2 =
     | CPatVar i1, CPatVar i2 ->
       Id.equal i1 i2
     | CEvar (id1, c1), CEvar (id2, c2) ->
-      Id.equal id1 id2 && List.equal instance_eq c1 c2
+      Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2
     | CSort s1, CSort s2 ->
       Glob_ops.glob_sort_eq s1 s2
     | CCast(t1,c1), CCast(t2,c2) ->
@@ -235,7 +235,7 @@ and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
   List.equal (List.equal local_binder_eq) bl1 bl2
 
 and instance_eq (x1,c1) (x2,c2) =
-  Id.equal x1 x2 && constr_expr_eq c1 c2
+  Id.equal x1.CAst.v x2.CAst.v && constr_expr_eq c1 c2
 
 and cast_expr_eq c1 c2 = match c1, c2 with
 | CastConv t1, CastConv t2
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 167ea3ecdf..e5a60769e8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -978,7 +978,7 @@ let rec extern inctx ?impargs scopes vars r =
       if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else
        (match kind with
          | Evar_kinds.SecondOrderPatVar n -> CPatVar n
-         | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[]))
+         | Evar_kinds.FirstOrderPatVar n -> CEvar (CAst.make n,[]))
 
   | GApp (f,args) ->
       (match DAst.get f with
@@ -1391,7 +1391,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       | None -> Id.of_string "__"
       | Some id -> id
       in
-      GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l)
+      GEvar (CAst.make id,List.map (fun (id,c) -> (CAst.make id, glob_of_pat avoid env sigma c)) l)
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
         | Name id   -> id
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 48fb4a4a5d..959b61a3d7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2188,7 +2188,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         GPatVar (Evar_kinds.SecondOrderPatVar n)
     | CEvar (n, []) when pattern_mode ->
         DAst.make ?loc @@
-        GPatVar (Evar_kinds.FirstOrderPatVar n)
+        GPatVar (Evar_kinds.FirstOrderPatVar n.CAst.v)
     (* end *)
     (* Parsing existential variables *)
     | CEvar (n, l) ->
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 1ec83c496a..644493a010 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -154,7 +154,7 @@ GRAMMAR EXTEND Gram
     | "10" LEFTA
       [ f = operconstr; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) }
       | "@"; f = global; i = univ_instance; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) }
-      | "@"; lid = pattern_identref; args = LIST1 identref ->
+      | "@"; lid = pattern_ident; args = LIST1 identref ->
         { let { CAst.loc = locid; v = id } = lid in
           let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
           CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ]
@@ -252,7 +252,7 @@ GRAMMAR EXTEND Gram
       | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ]
   ;
   appl_arg:
-    [ [ test_lpar_id_coloneq; "("; id = ident; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) }
+    [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) }
       | c=operconstr LEVEL "9" -> { (c,None) } ] ]
   ;
   atomic_constr:
@@ -261,12 +261,12 @@ GRAMMAR EXTEND Gram
       | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPrim (String s) }
       | "_"      -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
-      | "?"; "["; id = ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroIdentifier id, None) }
-      | "?"; "["; id = pattern_ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroFresh id, None) }
+      | "?"; "["; id = identref; "]"  -> { CAst.make ~loc @@  CHole (None, IntroIdentifier id.CAst.v, None) }
+      | "?"; "["; id = pattern_ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroFresh id.CAst.v, None) }
       | id = pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ]
   ;
   inst:
-    [ [ id = ident; ":="; c = lconstr -> { (id,c) } ] ]
+    [ [ id = identref; ":="; c = lconstr -> { (id,c) } ] ]
   ;
   evar_instance:
     [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l }
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 270662b824..8069f049fd 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -47,7 +47,7 @@ GRAMMAR EXTEND Gram
   GLOBAL:
     bignat bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
-    ne_string string lstring pattern_ident pattern_identref by_notation
+    ne_string string lstring pattern_ident by_notation
     smart_global bar_cbrace strategy_level;
   preident:
     [ [ s = IDENT -> { s } ] ]
@@ -56,10 +56,7 @@ GRAMMAR EXTEND Gram
     [ [ s = IDENT -> { Id.of_string s } ] ]
   ;
   pattern_ident:
-    [ [ LEFTQMARK; id = ident -> { id } ] ]
-  ;
-  pattern_identref:
-    [ [ id = pattern_ident -> { CAst.make ~loc id } ] ]
+    [ [ LEFTQMARK; id = ident -> { CAst.make ~loc id } ] ]
   ;
   var: (* as identref, but interpret as a term identifier in ltac *)
     [ [ id = ident -> { CAst.make ~loc id } ] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 723f08413e..fa7de40a30 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -286,7 +286,7 @@ module Prim =
     let univ_decl = Entry.create "univ_decl"
     let ident_decl = Entry.create "ident_decl"
     let pattern_ident = Entry.create "pattern_ident"
-    let pattern_identref = Entry.create "pattern_identref"
+    let pattern_identref = pattern_ident (* To remove in 8.14 *)
 
     (* A synonym of ident - maybe ident will be located one day *)
     let base_ident = Entry.create "base_ident"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ae9a7423c2..fa223367f7 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -156,8 +156,8 @@ module Prim :
     val identref : lident Entry.t
     val univ_decl : universe_decl_expr Entry.t
     val ident_decl : ident_decl Entry.t
-    val pattern_ident : Id.t Entry.t
-    val pattern_identref : lident Entry.t
+    val pattern_ident : lident Entry.t
+    val pattern_identref : lident Entry.t [@@ocaml.deprecated "Use Prim.pattern_identref"]
     val base_ident : Id.t Entry.t
     val bignat : string Entry.t
     val natural : int Entry.t
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index e51b1f051d..c186a83a5c 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -280,7 +280,7 @@ GRAMMAR EXTEND Gram
       | "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ]
   ;
   naming_intropattern:
-    [ [ prefix = pattern_ident -> { IntroFresh prefix }
+    [ [ prefix = pattern_ident -> { IntroFresh prefix.CAst.v }
       | "?" -> { IntroAnonymous }
       | id = ident -> { IntroIdentifier id } ] ]
   ;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 91c155fcce..a12a832f76 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -715,9 +715,9 @@ and detype_r d flags avoid env sigma t =
         (* Meta in constr are not user-parsable and are mapped to Evar *)
         if n = Constr_matching.special_meta then
           (* Using a dash to be unparsable *)
-          GEvar (Id.of_string_soft "CONTEXT-HOLE", [])
+          GEvar (CAst.make @@ Id.of_string_soft "CONTEXT-HOLE", [])
         else
-          GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
+          GEvar (CAst.make @@ Id.of_string_soft ("M" ^ string_of_int n), [])
     | Var id ->
         (* Discriminate between section variable and non-section variable *)
         (try let _ = Global.lookup_named id in GRef (GlobRef.VarRef id, None)
@@ -788,12 +788,12 @@ and detype_r d flags avoid env sigma t =
           let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
           let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match EConstr.kind sigma c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
           let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in
-          id,l
+          id,List.map (fun (id,c) -> (CAst.make id,c)) l
         with Not_found ->
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
-          (List.map (fun c -> (Id.of_string "__",c)) cl)
+          (List.map (fun c -> (CAst.make @@ Id.of_string "__",c)) cl)
       in
-        GEvar (id,
+        GEvar (CAst.make id,
                List.map (on_snd (detype d flags avoid env sigma)) l)
     | Ind (ind_sp,u) ->
         GRef (GlobRef.IndRef ind_sp, detype_instance sigma u)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5bd26be823..dc5fd80f9e 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -128,7 +128,7 @@ let fix_kind_eq k1 k2 = match k1, k2 with
   | (GFix _ | GCoFix _), _ -> false
 
 let instance_eq f (x1,c1) (x2,c2) =
-  Id.equal x1 x2 && f c1 c2
+  Id.equal x1.CAst.v x2.CAst.v && f c1 c2
 
 let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
   | GRef (gr1, u1), GRef (gr2, u2) ->
@@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     Option.equal (List.equal glob_level_eq) u1 u2
   | GVar id1, GVar id2 -> Id.equal id1 id2
   | GEvar (id1, arg1), GEvar (id2, arg2) ->
-    Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2
+    Id.equal id1.CAst.v id2.CAst.v && List.equal (instance_eq f) arg1 arg2
   | GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2
   | GApp (f1, arg1), GApp (f2, arg2) ->
     f f1 f2 && List.equal f arg1 arg2
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 526eac6f1e..a49c8abe26 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -75,7 +75,7 @@ type 'a glob_constr_r =
   | GVar of Id.t
       (** An identifier that cannot be regarded as "GRef".
           Bound variables are typically represented this way. *)
-  | GEvar   of existential_name * (Id.t * 'a glob_constr_g) list
+  | GEvar   of existential_name CAst.t * (lident * 'a glob_constr_g) list
   | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *)
   | GApp    of 'a glob_constr_g * 'a glob_constr_g list
   | GLambda of Name.t * binding_kind *  'a glob_constr_g * 'a glob_constr_g
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7597661ca8..8f52018a44 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -365,9 +365,9 @@ let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = functio
   | Some t ->
     Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t
 
-let check_instance loc subst = function
+let check_instance subst = function
   | [] -> ()
-  | (id,_) :: _ ->
+  | (CAst.{loc;v=id},_) :: _ ->
       if List.mem_assoc id subst then
         user_err ?loc  (Id.print id ++ str "appears more than once.")
       else
@@ -493,7 +493,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> ty
 type pretyper = {
   pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun;
   pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun;
-  pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun;
+  pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun;
   pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun;
   pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun;
   pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
@@ -587,10 +587,10 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk
           strbrk " is not well-typed.") in
     let sigma, c, update =
       try
-        let c = List.assoc id update in
+        let c = snd (List.find (fun (CAst.{v=id'},c) -> Id.equal id id') update) in
         let sigma, c = eval_pretyper self ~program_mode ~poly resolve_tc (mk_tycon t) env sigma c in
         check_body sigma id (Some c.uj_val);
-        sigma, c.uj_val, List.remove_assoc id update
+        sigma, c.uj_val, List.remove_first (fun (CAst.{v=id'},_) -> Id.equal id id') update
       with Not_found ->
       try
         let (n,b',t') = lookup_rel_id id (rel_context !!env) in
@@ -609,7 +609,7 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk
           str " in current context: no binding for " ++ Id.print id ++ str ".") in
     ((id,c)::subst, update, sigma) in
   let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in
-  check_instance loc subst inst;
+  check_instance subst inst;
   sigma, List.map snd subst
 
 module Default =
@@ -628,13 +628,13 @@ struct
     let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in
     discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon
 
-  let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma =
+  let pretype_evar self (CAst.{v=id;loc=locid}, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma =
       (* Ne faudrait-il pas s'assurer que hyps est bien un
          sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
       let id = interp_ltac_id env id in
       let evk =
         try Evd.evar_key id sigma
-        with Not_found -> error_evar_not_found ?loc !!env sigma id in
+        with Not_found -> error_evar_not_found ?loc:locid !!env sigma id in
       let hyps = evar_filtered_context (Evd.find sigma evk) in
       let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in
       let c = mkEvar (evk, args) in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c03374c59f..7bb4a6e273 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -148,7 +148,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> Ev
 type pretyper = {
   pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun;
   pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun;
-  pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun;
+  pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun;
   pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun;
   pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun;
   pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 267f5e0b5f..4200268acc 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -227,11 +227,11 @@ let tag_var = tag Tag.variable
 
   let pr_evar pr id l =
     hov 0 (
-      tag_evar (str "?" ++ pr_id id) ++
+      tag_evar (str "?" ++ pr_lident id) ++
         (match l with
           | [] -> mt()
           | l ->
-            let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in
+            let f (id,c) = pr_lident id ++ str ":=" ++ pr ltop c in
             str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}"))
 
   let las = lapp
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index dd372ecb0f..b2ebc61b4e 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -514,12 +514,12 @@ let match_goals ot nt =
     | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> ()
     | CPatVar _, CPatVar _ -> ()
     | CEvar (n,l), CEvar (n2,l2) ->
-      let oevar = if ogname = "" then Id.to_string n else ogname in
-      nevar_to_oevar := CString.Map.add (Id.to_string n2) oevar !nevar_to_oevar;
+      let oevar = if ogname = "" then Id.to_string n.CAst.v else ogname in
+      nevar_to_oevar := CString.Map.add (Id.to_string n2.CAst.v) oevar !nevar_to_oevar;
       iter2  (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2)  l l2
     | CEvar (n,l), nt' ->
       (* pass down the old goal evar name *)
-      match_goals_r (Id.to_string n) nt' nt'
+      match_goals_r (Id.to_string n.CAst.v) nt' nt'
     | CSort s, CSort s2 -> ()
     | CCast (c,c'), CCast (c2,c'2) ->
       constr_expr ogname c c2;
diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index b346b3ee5c..90f8008dc2 100644
--- a/user-contrib/Ltac2/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
@@ -229,7 +229,7 @@ let check_pattern_id ?loc id =
 let pattern_vars pat =
   let rec aux () accu pat = match pat.CAst.v with
   | Constrexpr.CPatVar id
-  | Constrexpr.CEvar (id, []) ->
+  | Constrexpr.CEvar ({CAst.v=id}, []) ->
     let loc = pat.CAst.loc in
     let () = check_pattern_id ?loc id in
     Id.Map.add id loc accu