From 9ad3bb77445de870eecf006941779c78531512e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 9 Jun 2020 14:17:25 +0200
Subject: 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.
---
 pretyping/globEnv.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'pretyping')

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 =
-- 
cgit v1.2.3