From 26e5194bc252e4ac71c74f8ac73a0e2cbe82edf6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Aug 2016 19:18:48 +0200
Subject: Using the extended contexts in pretyping.

In addition to sharing, we also delay the computation of the environment in
a by-need fashion.
---
 engine/evarutil.ml  | 4 ++++
 engine/evarutil.mli | 8 ++++----
 2 files changed, 8 insertions(+), 4 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b3a886f711..b3e17fa9d2 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -302,6 +302,10 @@ let next_name_away na avoid =
   let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in
   next_ident_away_from id avoid
 
+type ext_named_context =
+  Vars.substl * (Id.t * Constr.constr) list *
+  Id.Set.t * Context.Named.t
+
 let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
   let open Context.Named.Declaration in
   let replace_var_named_declaration id0 id decl =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 45f0d6b078..429ea73de1 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -199,13 +199,13 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
 val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
   Id.Set.t -> named_context_val * types * types
 
-val push_rel_decl_to_named_context :
-  Context.Rel.Declaration.t ->
+type ext_named_context =
   Vars.substl * (Id.t * Constr.constr) list *
-  Id.Set.t * Context.Named.t ->
-  Term.constr list * (Id.t * Constr.constr) list *
   Id.Set.t * Context.Named.t
 
+val push_rel_decl_to_named_context :
+  Context.Rel.Declaration.t -> ext_named_context -> ext_named_context
+
 val push_rel_context_to_named_context : Environ.env -> types ->
   named_context_val * types * constr list * constr list * (identifier*constr) list
 
-- 
cgit v1.2.3