merge

1 files changed, 6 insertions, 7 deletions

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index f403116617..1e95a3564d 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Declarations
 
 (** The type of environments. *)
@@ -45,9 +44,9 @@ type named_vals = (Id.t * lazy_val) list
 
 type env = {
     env_globals       : globals;
-    env_named_context : named_context;
+    env_named_context : Context.Named.t;
     env_named_vals    : named_vals;
-    env_rel_context   : rel_context;
+    env_rel_context   : Context.Rel.t;
     env_rel_val       : lazy_val list;
     env_nb_rel        : int;
     env_stratification : stratification;
@@ -56,7 +55,7 @@ type env = {
     indirect_pterms : Opaqueproof.opaquetab;
 }
 
-type named_context_val = named_context * named_vals
+type named_context_val = Context.Named.t * named_vals
 
 val empty_named_context_val : named_context_val
 
@@ -65,15 +64,15 @@ 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.Named.Declaration.t -> env -> env
 val lookup_named_val : Id.t -> env -> lazy_val
 val env_of_named     : Id.t -> env -> env