COMMENT: Pre_env.env

1 files changed, 2 insertions, 2 deletions

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 6bfba2d40b..48d7ee9ec3 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -68,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;