Use the evarinfo-stored identity substitution where applicable.

2 files changed, 4 insertions, 10 deletions

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) ->