Actually use the default instance stored inside named_context_val.

4 files changed, 9 insertions, 9 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 334c23c963..36297fe243 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -743,6 +743,9 @@ let match_named_context_val :
   match unsafe_eq with
   | Refl -> match_named_context_val
 
+let identity_subst_val : named_context_val -> t list =
+  match unsafe_eq with Refl -> fun ctx -> ctx.env_named_var
+
 let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
   evd, t
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index d0f675319d..a018f4064f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -326,6 +326,8 @@ val map_rel_context_in_env :
 val match_named_context_val :
   named_context_val -> (named_declaration * lazy_val * named_context_val) option
 
+val identity_subst_val : named_context_val -> t list
+
 (* XXX Missing Sigma proxy *)
 val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index c3f189cdf0..01c4e5fd72 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -386,14 +386,12 @@ let push_rel_decl_to_named_context
 
 let push_rel_context_to_named_context ?hypnaming env sigma typ =
   (* compute the instances relative to the named context and rel_context *)
-  let open Context.Named.Declaration in
   let open EConstr in
-  let ids = List.map get_id (named_context env) in
-  let inst_vars = List.map mkVar ids in
+  let inst_vars = EConstr.identity_subst_val (named_context_val env) in
   if List.is_empty (Environ.rel_context env) then
     (named_context_val env, typ, inst_vars, empty_csubst)
   else
-    let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
+    let avoid = Environ.ids_of_named_context_val (named_context_val env) in
     let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
     (* move the rel context to a named context and extend the named instance *)
     (* with vars of the rel context *)
diff --git a/engine/evd.ml b/engine/evd.ml
index 5d50472696..6bbfddd988 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -152,9 +152,7 @@ struct
   let make s = ref (Some s)
   let none () = ref None
   let repr sign filter s = match !s with
-  | None ->
-    let fsign = Filter.filter_list filter (named_context_of_val sign) in
-    List.map (NamedDecl.get_id %> mkVar) fsign
+  | None -> Filter.filter_list filter sign.env_named_var
   | Some s -> s
   let is_identity l s = match !s with
   | None -> false
@@ -810,8 +808,7 @@ let declare_restricted_evar evar_flags evk evk' =
 let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
-  let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in
+  let id_inst = Filter.filter_list filter evar_info.evar_hyps.env_named_var in
   let evar_info' =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;