Actually use the default instance stored inside named_context_val.

8 files changed, 15 insertions, 23 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;
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1b7768852e..d7996a722a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1352,7 +1352,7 @@ let unsafe_intro env decl b =
   Refine.refine ~typecheck:false begin fun sigma ->
     let ctx = Environ.named_context_val env in
     let nctx = EConstr.push_named_context_val decl ctx in
-    let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in
+    let inst = EConstr.identity_subst_val (Environ.named_context_val env) in
     let ninst = EConstr.mkRel 1 :: inst in
     let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
     let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 81a62a7048..34fae613bf 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -33,8 +33,6 @@ type t = {
   (** For locating indices *)
   renamed_env : env;
   (** For name management *)
-  renamed_vars : EConstr.t list Lazy.t;
-  (** Identity instance of named_context of renamed_env, to maximize sharing *)
   extra : ext_named_context Lazy.t;
   (** Delay the computation of the evar extended environment *)
   lvar : ltac_var_map;
@@ -45,11 +43,9 @@ let make ~hypnaming env sigma lvar =
     let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
     Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
       (rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in
-  let open Context.Named.Declaration in
   {
     static_env = env;
     renamed_env = env;
-    renamed_vars = lazy (List.map (get_id %> mkVar) (named_context env));
     extra = lazy (get_extra env sigma);
     lvar = lvar;
   }
@@ -76,7 +72,6 @@ let push_rel ~hypnaming sigma d env =
   let env = {
     static_env = push_rel d env.static_env;
     renamed_env = push_rel d' env.renamed_env;
-    renamed_vars = env.renamed_vars;
     extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
@@ -89,7 +84,6 @@ let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env =
   let env = {
     static_env = push_rel_context ctx env.static_env;
     renamed_env = push_rel_context ctx' env.renamed_env;
-    renamed_vars = env.renamed_vars;
     extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
@@ -102,7 +96,7 @@ let push_rec_types ~hypnaming sigma (lna,typarray) env =
   Array.map get_annot ctx, env
 
 let new_evar env sigma ?src ?naming typ =
-  let lazy inst_vars = env.renamed_vars in
+  let inst_vars = EConstr.identity_subst_val (named_context_val env.renamed_env) in
   let rec rel_list n accu =
     if n <= 0 then accu
     else rel_list (n - 1) (mkRel n :: accu)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 70c09df241..1c3aed8fc2 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Pp
 
 module NamedDecl = Context.Named.Declaration
@@ -58,8 +57,7 @@ module V82 = struct
        goals are restored to their initial value after the evar is
        created. *)
     let prev_future_goals = Evd.save_future_goals evars in
-    let ctxt = Environ.named_context_of_val hyps in
-    let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in
+    let inst = EConstr.identity_subst_val hyps in
     let (evars, evk) =
       Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false ~identity:inst hyps evars concl
     in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f60151838a..cb2e607012 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -117,7 +117,7 @@ let unsafe_intro env decl b =
   Refine.refine ~typecheck:false begin fun sigma ->
     let ctx = named_context_val env in
     let nctx = push_named_context_val decl ctx in
-    let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
+    let inst = identity_subst_val (named_context_val env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
     let (sigma, ev) = new_pure_evar nctx sigma nb ~principal:true in
@@ -338,7 +338,7 @@ let rename_hyp repl =
       let nhyps = List.map map hyps in
       let nconcl = subst concl in
       let nctx = val_of_named_context nhyps in
-      let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
+      let instance = EConstr.identity_subst_val (Environ.named_context_val env) in
       Refine.refine ~typecheck:false begin fun sigma ->
         let sigma, ev = Evarutil.new_pure_evar nctx sigma nconcl ~principal:true in
         sigma, mkEvar (ev, instance)
@@ -2783,7 +2783,7 @@ let pose_tac na c =
       let id = make_annot id Sorts.Relevant in
       let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in
       let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in
-      let inst = List.map (fun d -> mkVar (get_id d)) (named_context env) in
+      let inst = EConstr.identity_subst_val hyps in
       let body = mkEvar (ev, mkRel 1 :: inst) in
       (sigma, mkLetIn (map_annot Name.mk_name id, c, t, body))
     end