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

Reviewed-by: ppedrot

4 files changed, 6 insertions, 6 deletions

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) ->