1 files changed, 9 insertions, 20 deletions

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index f211583e06..48d7ee9ec3 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -17,7 +17,8 @@ open Util
 open Names
 open Term
 open Declarations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 (* The type of environments. *)
 
@@ -67,8 +68,8 @@ type named_context_val = {
 }
 
 type env = {
-  env_globals       : globals;
-  env_named_context : named_context_val;
+  env_globals       : globals;           (* globals = constants + inductive types + modules + module-types *)
+  env_named_context : named_context_val; (* section variables *)
   env_rel_context   : Context.Rel.t;
   env_rel_val       : lazy_val list;
   env_nb_rel        : int;
@@ -128,10 +129,10 @@ let env_of_rel n env =
 (* Named context *)
 
 let push_named_context_val_val d rval ctxt =
-(*   assert (not (Id.Map.mem (get_id d) ctxt.env_named_map)); *)
+(*   assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *)
   {
     env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
-    env_named_map = Id.Map.add (get_id d) (d, rval) ctxt.env_named_map;
+    env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map;
   }
 
 let push_named_context_val d ctxt =
@@ -140,8 +141,8 @@ let push_named_context_val d ctxt =
 let match_named_context_val c = match c.env_named_ctx with
 | [] -> None
 | decl :: ctx ->
-  let (_, v) = Id.Map.find (get_id decl) c.env_named_map in
-  let map = Id.Map.remove (get_id decl) c.env_named_map in
+  let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in
+  let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in
   let cval = { env_named_ctx = ctx; env_named_map = map } in
   Some (decl, v, cval)
 
@@ -160,19 +161,7 @@ let map_named_val f ctxt =
   else { env_named_ctx = ctx; env_named_map = map }
 
 let push_named d env =
-(*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
-  assert (env.env_rel_context = []); *)
-  { env_globals = env.env_globals;
-    env_named_context = push_named_context_val d env.env_named_context;
-    env_rel_context = env.env_rel_context;
-    env_rel_val = env.env_rel_val;
-    env_nb_rel = env.env_nb_rel;
-    env_stratification = env.env_stratification;
-    env_typing_flags = env.env_typing_flags;
-    env_conv_oracle = env.env_conv_oracle;
-    retroknowledge = env.retroknowledge;
-    indirect_pterms = env.indirect_pterms;
-  }
+  {env with env_named_context = push_named_context_val d env.env_named_context}
 
 let lookup_named id env =
   fst (Id.Map.find id env.env_named_context.env_named_map)