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.
---
 kernel/environ.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 79e632daa0..f489b13a3b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -176,6 +176,8 @@ val named_body : variable -> env -> constr option
 val fold_named_context :
   (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
+val match_named_context_val : named_context_val -> (named_declaration * lazy_val * named_context_val) option
+
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
   ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a
-- 
cgit v1.2.3