diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 5 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 9 | ||||
| -rw-r--r-- | pretyping/globEnv.ml | 8 |
3 files changed, 5 insertions, 17 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) -> 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) |