Add location in existential variable names (CEvar/GEvar).

5 files changed, 9 insertions, 9 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 503035c6c3..c5df5d7968 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)
@@ -793,7 +793,7 @@ and detype_r d flags avoid env sigma t =
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
           (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 fd6083abd1..dc5fd80f9e 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -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 04e9382015..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 * (lident * '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 9c400da4ae..f79c4f4e96 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -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 * (lident * 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;
@@ -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 c4f0f18e27..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 * (lident * 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;