1 files changed, 20 insertions, 13 deletions

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 23f9a3f4..86679036 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -8,9 +8,7 @@
 
 open Names
 open Term
-open Context
 open Declarations
-open Univ
 
 (** The type of environments. *)
 
@@ -19,7 +17,7 @@ type link_info =
   | LinkedInteractive of string
   | NotLinked
 
-type key = int Ephemeron.key option ref 
+type key = int CEphemeron.key option ref 
 
 type constant_key = constant_body * (link_info ref * key)
 
@@ -32,7 +30,7 @@ type globals = {
   env_modtypes : module_type_body MPmap.t}
 
 type stratification = {
-  env_universes : universes;
+  env_universes : UGraph.t;
   env_engagement : engagement
 }
 
@@ -42,23 +40,24 @@ val force_lazy_val : lazy_val -> (values * Id.Set.t) option
 val dummy_lazy_val : unit -> lazy_val
 val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit
 
-type named_vals = (Id.t * lazy_val) list
+type named_context_val = private {
+  env_named_ctx : Context.Named.t;
+  env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
+}
 
 type env = {
     env_globals       : globals;
-    env_named_context : named_context;
-    env_named_vals    : named_vals;
-    env_rel_context   : rel_context;
+    env_named_context : named_context_val;
+    env_rel_context   : Context.Rel.t;
     env_rel_val       : lazy_val list;
     env_nb_rel        : int;
     env_stratification : stratification;
+    env_typing_flags  : typing_flags;
     env_conv_oracle   : Conv_oracle.oracle;
     retroknowledge : Retroknowledge.retroknowledge;
     indirect_pterms : Opaqueproof.opaquetab;
 }
 
-type named_context_val = named_context * named_vals
-
 val empty_named_context_val : named_context_val
 
 val empty_env : env
@@ -66,15 +65,23 @@ val empty_env : env
 (** Rel context *)
 
 val nb_rel         : env -> int
-val push_rel       : rel_declaration -> env -> env
+val push_rel       : Context.Rel.Declaration.t -> env -> env
 val lookup_rel_val : int -> env -> lazy_val
 val env_of_rel     : int -> env -> env
 
 (** Named context *)
 
 val push_named_context_val  :
-    named_declaration -> named_context_val -> named_context_val
-val push_named       : named_declaration -> env -> env
+    Context.Named.Declaration.t -> named_context_val -> named_context_val
+val push_named_context_val_val  :
+    Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val
+val match_named_context_val  :
+  named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option
+val map_named_val :
+   (constr -> constr) -> named_context_val -> named_context_val
+
+val push_named       : Context.Named.Declaration.t -> env -> env
+val lookup_named     : Id.t -> env -> Context.Named.Declaration.t
 val lookup_named_val : Id.t -> env -> lazy_val
 val env_of_named     : Id.t -> env -> env