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.
---
 engine/eConstr.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9a73c3e3f5..aea441b90b 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -322,6 +322,9 @@ val lookup_named_val : variable -> named_context_val -> named_declaration
 val map_rel_context_in_env :
   (env -> constr -> constr) -> env -> rel_context -> rel_context
 
+val match_named_context_val :
+  named_context_val -> (named_declaration * lazy_val * named_context_val) option
+
 (* XXX Missing Sigma proxy *)
 val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
-- 
cgit v1.2.3