Adding and using locations on identifiers in constr_expr where they were missing.

5 files changed, 11 insertions, 11 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 7fcb0795bd..503035c6c3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -788,10 +788,10 @@ 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,
                List.map (on_snd (detype d flags avoid env sigma)) l)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5bd26be823..fd6083abd1 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) ->
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 526eac6f1e..04e9382015 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 * (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 b9825b6a92..9c400da4ae 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 * (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 =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c03374c59f..c4f0f18e27 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 * (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;