diff options
| -rw-r--r-- | pretyping/globEnv.ml | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index e458d030cb..05abb86f46 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -33,6 +33,8 @@ 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; @@ -43,9 +45,11 @@ 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; } @@ -67,10 +71,12 @@ let ltac_interp_id { ltac_idents ; ltac_genargs } id = let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar) let push_rel ~hypnaming sigma d env = - let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in + let open Context.Rel.Declaration in + let d' = map_name (ltac_interp_name env.lvar) d in 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 @@ -83,6 +89,7 @@ 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 @@ -95,12 +102,14 @@ let push_rec_types ~hypnaming sigma (lna,typarray) env = Array.map get_annot ctx, env let new_evar env sigma ?src ?naming typ = - let open Context.Named.Declaration in - let inst_vars = List.map (get_id %> mkVar) (named_context env.renamed_env) in - let inst_rels = List.rev (rel_list 0 (nb_rel env.renamed_env)) in + let lazy inst_vars = env.renamed_vars in + let rec rel_list n accu = + if n <= 0 then accu + else rel_list (n - 1) (mkRel n :: accu) + in + let instance = rel_list (nb_rel env.renamed_env) inst_vars in let (subst, _, sign) = Lazy.force env.extra in let typ' = csubst_subst subst typ in - let instance = inst_rels @ inst_vars in new_evar_instance sign sigma typ' ?src ?naming instance let new_type_evar env sigma ~src = |