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.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index ca681e58f8..42c9359ff0 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -733,6 +733,11 @@ let map_rel_context_in_env f env sign =
   in
   aux env [] (List.rev sign)
 
+let match_named_context_val :
+  named_context_val -> (named_declaration * lazy_val * named_context_val) option =
+  match unsafe_eq with
+  | Refl -> match_named_context_val
+
 let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
   evd, t
-- 
cgit v1.2.3