Merge PR #12725: Store evar identity instances in evarinfo / named_context_val

Ack-by: SkySkimmer
Reviewed-by: gares

14 files changed, 107 insertions, 51 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 b4b2032dd2..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 *)
@@ -409,8 +407,9 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
 
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
-let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
-    ?candidates ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ =
+let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?identity
+  ?(abstract_arguments = Abstraction.identity) ?candidates
+  ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ =
   let name = match naming with
   | IntroAnonymous -> None
   | IntroIdentifier id -> Some id
@@ -419,6 +418,10 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a
     let id = Namegen.next_ident_away_from id has_name in
     Some id
   in
+  let identity = match identity with
+  | None -> Identity.none ()
+  | Some inst -> Identity.make inst
+  in
   let evi = {
     evar_hyps = sign;
     evar_concl = typ;
@@ -426,7 +429,9 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a
     evar_filter = filter;
     evar_abstract_arguments = abstract_arguments;
     evar_source = src;
-    evar_candidates = candidates }
+    evar_candidates = candidates;
+    evar_identity = identity;
+  }
   in
   let typeclass_candidate = if principal then Some false else typeclass_candidate in
   let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in
@@ -447,7 +452,8 @@ let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_can
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
+  let identity = if Int.equal (Environ.nb_rel env) 0 then Some instance else None in
+  let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?identity ?abstract_arguments ?candidates ?naming
     ?typeclass_candidate ?principal in
   (evd, EConstr.mkEvar (evk, instance))
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 41b58d38b0..a8fc9ef5e2 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -40,8 +40,18 @@ val new_evar :
   ?principal:bool -> ?hypnaming:naming_mode ->
   env -> evar_map -> types -> evar_map * EConstr.t
 
+(** Low-level interface to create an evar.
+  @param src User-facing source for the evar
+  @param filter See {!Evd.Filter}, must be the same length as [named_context_val]
+  @param identity See {!Evd.Identity}, must be the name projection of [named_context_val]
+  @param naming A naming scheme for the evar
+  @param principal Whether the evar is the principal goal
+  @param named_context_val The context of the evar
+  @param types The type of conclusion of the evar
+*)
 val new_pure_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?identity:EConstr.t list ->
   ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?typeclass_candidate:bool ->
diff --git a/engine/evd.ml b/engine/evd.ml
index e85cbc96b2..92657c41a9 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -139,6 +139,29 @@ module Abstraction = struct
   let abstract_last l = Abstract :: l
 end
 
+module Identity :
+sig
+  type t
+  val make : econstr list -> t
+  val none : unit -> t
+  val repr : named_context_val -> Filter.t -> t -> econstr list
+  val is_identity : econstr list -> t -> bool
+end =
+struct
+  type t = econstr list option ref
+  let make s = ref (Some s)
+  let none () = ref None
+  let repr sign filter s = match !s with
+  | None ->
+    let ans = Filter.filter_list filter sign.env_named_var in
+    let () = s := Some ans in
+    ans
+  | Some s -> s
+  let is_identity l s = match !s with
+  | None -> false
+  | Some s -> s == l
+end
+
 (* The kinds of existential variables are now defined in [Evar_kinds] *)
 
 (* The type of mappings for existential variables *)
@@ -158,7 +181,9 @@ type evar_info = {
   evar_filter : Filter.t;
   evar_abstract_arguments : Abstraction.t;
   evar_source : Evar_kinds.t Loc.located;
-  evar_candidates : constr list option; (* if not None, list of allowed instances *)}
+  evar_candidates : constr list option; (* if not None, list of allowed instances *)
+  evar_identity : Identity.t;
+}
 
 let make_evar hyps ccl = {
   evar_concl = ccl;
@@ -167,7 +192,9 @@ let make_evar hyps ccl = {
   evar_filter = Filter.identity;
   evar_abstract_arguments = Abstraction.identity;
   evar_source = Loc.tag @@ Evar_kinds.InternalHole;
-  evar_candidates = None; }
+  evar_candidates = None;
+  evar_identity = Identity.none ();
+}
 
 let instance_mismatch () =
   anomaly (Pp.str "Signature and its instance do not match.")
@@ -216,6 +243,9 @@ let evar_filtered_env env evi = match Filter.repr (evar_filter evi) with
   in
   make_env filter (evar_context evi)
 
+let evar_identity_subst evi =
+  Identity.repr evi.evar_hyps evi.evar_filter evi.evar_identity
+
 let map_evar_body f = function
   | Evar_empty -> Evar_empty
   | Evar_defined d -> Evar_defined (f d)
@@ -256,7 +286,9 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) args
 
 let make_evar_instance_array info args =
-  evar_instance_array (NamedDecl.get_id %> isVarId) info args
+  if Identity.is_identity args info.evar_identity then []
+  else
+    evar_instance_array (NamedDecl.get_id %> isVarId) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -779,16 +811,17 @@ 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 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;
-      evar_source = (match src with None -> evar_info.evar_source | Some src -> src) } in
+      evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
+      evar_identity = Identity.make id_inst;
+    } in
   let last_mods = match evd.conv_pbs with
   | [] ->  evd.last_mods
   | _ -> Evar.Set.add evk evd.last_mods in
   let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
-  let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
diff --git a/engine/evd.mli b/engine/evd.mli
index 3f17e63034..d338b06e0e 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -89,6 +89,15 @@ module Abstraction : sig
   val abstract_last : t -> t
 end
 
+module Identity :
+sig
+  type t
+  (** Identity substitutions *)
+
+  val make : econstr list -> t
+  val none : unit -> t
+end
+
 (** {6 Evar infos} *)
 
 type evar_body =
@@ -114,6 +123,9 @@ type evar_info = {
   (** Information about the evar. *)
   evar_candidates : econstr list option;
   (** List of possible solutions when known that it is a finite list *)
+  evar_identity : Identity.t;
+  (** Default evar instance, i.e. a list of Var nodes projected from the
+      filtered environment. *)
 }
 
 val make_evar : named_context_val -> etypes -> evar_info
@@ -127,6 +139,7 @@ val evar_candidates : evar_info -> constr list option
 val evar_filter : evar_info -> Filter.t
 val evar_env : env -> evar_info -> env
 val evar_filtered_env : env -> evar_info -> env
+val evar_identity_subst : evar_info -> econstr list
 
 val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body
 val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e75ccbb252..03c9cb4be6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -87,6 +87,7 @@ let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
 type named_context_val = {
   env_named_ctx : Constr.named_context;
   env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
+  env_named_var : Constr.t list;
 }
 
 type rel_context_val = {
@@ -109,6 +110,7 @@ type env = {
 let empty_named_context_val = {
   env_named_ctx = [];
   env_named_map = Id.Map.empty;
+  env_named_var = [];
 }
 
 let empty_rel_context_val = {
@@ -183,6 +185,7 @@ let push_named_context_val_val d rval ctxt =
   {
     env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
     env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map;
+    env_named_var = mkVar (NamedDecl.get_id d) :: ctxt.env_named_var;
   }
 
 let push_named_context_val d ctxt =
@@ -193,7 +196,7 @@ let match_named_context_val c = match c.env_named_ctx with
 | decl :: ctx ->
   let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in
   let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in
-  let cval = { env_named_ctx = ctx; env_named_map = map } in
+  let cval = { env_named_ctx = ctx; env_named_map = map; env_named_var = List.tl c.env_named_var } in
   Some (decl, v, cval)
 
 let map_named_val f ctxt =
@@ -208,7 +211,7 @@ let map_named_val f ctxt =
   in
   let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in
   if map == ctxt.env_named_map then ctxt
-  else { env_named_ctx = ctx; env_named_map = map }
+  else { env_named_ctx = ctx; env_named_map = map; env_named_var = ctxt.env_named_var }
 
 let push_named d env =
   {env with env_named_context = push_named_context_val d env.env_named_context}
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 5cb56a2a29..974e794c6b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -69,6 +69,11 @@ type stratification = {
 type named_context_val = private {
   env_named_ctx : Constr.named_context;
   env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
+  (** Identifier-indexed version of [env_named_ctx] *)
+  env_named_var : Constr.t list;
+  (** List of identifiers in [env_named_ctx], in the same order, including
+      let-ins. This is not used in the kernel, but is critical to preserve
+      sharing of evar instances in the proof engine. *)
 }
 
 type rel_context_val = private {
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/evarconv.ml b/pretyping/evarconv.ml
index 2feae8cc25..489e8de602 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1352,9 +1352,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
     (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs);
      Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar));
   let args = List.map (nf_evar evd) args in
-  let vars = List.map NamedDecl.get_id ctxt in
-  let argsubst = List.map2 (fun id c -> (id, c)) vars args in
-  let instance = List.map mkVar vars in
+  let argsubst = List.map2 (fun decl c -> (NamedDecl.get_id decl, c)) ctxt args in
+  let instance = evar_identity_subst evi in
   let rhs = nf_evar evd rhs in
   if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd);
   (* Ensure that any progress made by Typing.e_solve_evars will not contradict
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 79839099f7..989fb05c3d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -216,9 +216,6 @@ type 'a update =
 | UpdateWith of 'a
 | NoUpdate
 
-open Context.Named.Declaration
-let inst_of_vars sign = List.map (get_id %> mkVar) sign
-
 let restrict_evar_key evd evk filter candidates =
   match filter, candidates with
   | None, NoUpdate -> evd, evk
@@ -701,8 +698,7 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
   let (evd, evk) = new_pure_evar sign evd ty_t_in_sign ~filter ~src in
   let t_in_env = whd_evar evd t_in_env in
   let evd = define_fun env evd None (evk, inst_in_env) t_in_env in
-  let ctxt = named_context_of_val sign in
-  let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
+  let inst_in_sign = evar_identity_subst (Evd.find evd evk) in
   let evar_in_sign = mkEvar (evk, inst_in_sign) in
   (evd,whd_evar evd evar_in_sign)
 
@@ -735,9 +731,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let sign1 = evar_hyps evi1 in
   let filter1 = evar_filter evi1 in
   let src = subterm_source evk1 evi1.evar_source in
-  let ids1 = List.map get_id (named_context_of_val sign1) in
   let avoid = Environ.ids_of_named_context_val sign1 in
-  let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in
+  let inst_in_sign = evar_identity_subst evi1 in
   let open Context.Rel.Declaration in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
     List.fold_right (fun d (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
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 beeaa60433..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,12 +57,11 @@ 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 inst = EConstr.identity_subst_val hyps in
     let (evars, evk) =
-      Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false hyps evars concl
+      Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false ~identity:inst hyps evars concl
     in
     let evars = Evd.restore_future_goals evars prev_future_goals in
-    let ctxt = Environ.named_context_of_val hyps in
-    let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in
     let ev = EConstr.mkEvar (evk,inst) in
     (evk, ev, evars)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f553a290f9..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)
@@ -437,11 +437,6 @@ let clear_hyps2 env sigma ids sign t cl =
   with Evarutil.ClearDependencyError (id,err,inglobal) ->
     error_replacing_dependency env sigma id err inglobal
 
-let new_evar_from_context ?principal sign evd typ =
-  let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
-  let (evd, evk) = Evarutil.new_pure_evar sign evd typ in
-  (evd, mkEvar (evk, instance))
-
 let internal_cut ?(check=true) replace id t =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -449,22 +444,22 @@ let internal_cut ?(check=true) replace id t =
     let concl = Proofview.Goal.concl gl in
     let sign = named_context_val env in
     let r = Retyping.relevance_of_type env sigma t in
-    let sign',t,concl,sigma =
+    let env',t,concl,sigma =
       if replace then
         let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
         let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
         let sign' = insert_decl_in_named_context env sigma (LocalAssum (make_annot id r,t)) nexthyp sign' in
-        sign',t,concl,sigma
+        Environ.reset_with_named_context sign' env,t,concl,sigma
       else
         (if check && mem_named_context_val id sign then
            user_err (str "Variable " ++ Id.print id ++ str " is already declared.");
-         push_named_context_val (LocalAssum (make_annot id r,t)) sign,t,concl,sigma) in
+         push_named (LocalAssum (make_annot id r,t)) env,t,concl,sigma) in
     let nf_t = nf_betaiota env sigma t in
     Proofview.tclTHEN
       (Proofview.Unsafe.tclEVARS sigma)
       (Refine.refine ~typecheck:false begin fun sigma ->
-        let (sigma, ev) = new_evar_from_context sign sigma nf_t in
-        let (sigma, ev') = new_evar_from_context sign' sigma ~principal:true concl in
+        let (sigma, ev) = Evarutil.new_evar env sigma nf_t in
+        let (sigma, ev') = Evarutil.new_evar ~principal:true env' sigma concl in
         let term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var id ev') in
         (sigma, term)
       end)
@@ -2788,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