Do not reallocate named_context_val of the pretyping environment.

Instead of costly linear reallocations, we share as much as possible of the
prefixes of the various environment subcomponents.

1 files changed, 2 insertions, 3 deletions

diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index fad41614b4..e458d030cb 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -42,7 +42,7 @@ let make ~hypnaming env sigma lvar =
   let get_extra env sigma =
     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 env) in
+      (rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in
   {
     static_env = env;
     renamed_env = env;
@@ -98,10 +98,9 @@ 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 (subst, _, nc) = Lazy.force env.extra in
+  let (subst, _, sign) = Lazy.force env.extra in
   let typ' = csubst_subst subst typ in
   let instance = inst_rels @ inst_vars in
-  let sign = val_of_named_context nc in
   new_evar_instance sign sigma typ' ?src ?naming instance
 
 let new_type_evar env sigma ~src =