(Partially) Revert "Make Environ.globals abstract."

This (partially) reverts commit 3984f3c1db51f7b788ad49eafb7647774e8d1f53.

This broke clients wanting to inspect the enviroment, see
https://github.com/coq/coq/pull/7745#issuecomment-411597610

There is a need for clients to inspect the global environment, we keep
the record private as to concerns regarding its use, so even if no
function in the kernel is taking a `globals` as an input, we transmit
to clients its read-only nature.

We take the opportunity to refactor the record into a module with
scoped constructors.

2 files changed, 50 insertions, 32 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4a2aeea22d..98d66cafa1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -50,12 +50,19 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
-type globals = {
-  env_constants : constant_key Cmap_env.t;
-  env_inductives : mind_key Mindmap_env.t;
-  env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body MPmap.t;
-}
+module Globals = struct
+
+  type view =
+    { constants : constant_key Cmap_env.t
+    ; inductives : mind_key Mindmap_env.t
+    ; modules : module_body MPmap.t
+    ; modtypes : module_type_body MPmap.t
+    }
+
+  type t = view
+
+  let view x = x
+end
 
 type stratification = {
   env_universes : UGraph.t;
@@ -88,7 +95,7 @@ type rel_context_val = {
 }
 
 type env = {
-  env_globals       : globals;
+  env_globals       : Globals.t;
   env_named_context : named_context_val; (* section variables *)
   env_rel_context   : rel_context_val;
   env_nb_rel        : int;
@@ -110,11 +117,12 @@ let empty_rel_context_val = {
 }
 
 let empty_env = {
-  env_globals = {
-    env_constants = Cmap_env.empty;
-    env_inductives = Mindmap_env.empty;
-    env_modules = MPmap.empty;
-    env_modtypes = MPmap.empty};
+  env_globals =
+    { Globals.constants = Cmap_env.empty
+    ; inductives = Mindmap_env.empty
+    ; modules = MPmap.empty
+    ; modtypes = MPmap.empty
+    };
   env_named_context = empty_named_context_val;
   env_rel_context = empty_rel_context_val;
   env_nb_rel = 0;
@@ -215,29 +223,29 @@ let lookup_named_ctxt id ctxt =
   fst (Id.Map.find id ctxt.env_named_map)
 
 let fold_constants f env acc =
-  Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc
+  Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.constants acc
 
 let fold_inductives f env acc =
-  Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc
+  Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.inductives acc
 
 (* Global constants *)
 
 let lookup_constant_key kn env =
-  Cmap_env.find kn env.env_globals.env_constants
+  Cmap_env.find kn env.env_globals.Globals.constants
 
 let lookup_constant kn env =
-  fst (Cmap_env.find kn env.env_globals.env_constants)
+  fst (Cmap_env.find kn env.env_globals.Globals.constants)
 
 (* Mutual Inductives *)
 let lookup_mind kn env =
-  fst (Mindmap_env.find kn env.env_globals.env_inductives)
+  fst (Mindmap_env.find kn env.env_globals.Globals.inductives)
 
 let mind_context env mind =
   let mib = lookup_mind mind env in
   Declareops.inductive_polymorphic_context mib
 
 let lookup_mind_key kn env =
-  Mindmap_env.find kn env.env_globals.env_inductives
+  Mindmap_env.find kn env.env_globals.Globals.inductives
 
 let oracle env = env.env_typing_flags.conv_oracle
 let set_oracle env o =
@@ -468,10 +476,10 @@ let no_link_info = NotLinked
 
 let add_constant_key kn cb linkinfo env =
   let new_constants =
-    Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.env_constants in
+    Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.Globals.constants in
   let new_globals =
     { env.env_globals with
-	env_constants = new_constants } in
+        Globals.constants = new_constants } in
   { env with env_globals = new_globals }
 
 let add_constant kn cb env =
@@ -598,10 +606,10 @@ let template_polymorphic_pind (ind,u) env =
   else template_polymorphic_ind ind env
   
 let add_mind_key kn (_mind, _ as mind_key) env =
-  let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
+  let new_inds = Mindmap_env.add kn mind_key env.env_globals.Globals.inductives in
   let new_globals =
     { env.env_globals with
-        env_inductives = new_inds; } in
+        Globals.inductives = new_inds; } in
   { env with env_globals = new_globals }
 
 let add_mind kn mib env =
@@ -688,22 +696,22 @@ let keep_hyps env needed =
 
 let add_modtype mtb env =
   let mp = mtb.mod_mp in
-  let new_modtypes = MPmap.add mp mtb env.env_globals.env_modtypes in
-  let new_globals = { env.env_globals with env_modtypes = new_modtypes } in
+  let new_modtypes = MPmap.add mp mtb env.env_globals.Globals.modtypes in
+  let new_globals = { env.env_globals with Globals.modtypes = new_modtypes } in
   { env with env_globals = new_globals }
 
 let shallow_add_module mb env =
   let mp = mb.mod_mp in
-  let new_mods = MPmap.add mp mb env.env_globals.env_modules in
-  let new_globals = { env.env_globals with env_modules = new_mods } in
+  let new_mods = MPmap.add mp mb env.env_globals.Globals.modules in
+  let new_globals = { env.env_globals with Globals.modules = new_mods } in
   { env with env_globals = new_globals }
 
 let lookup_module mp env =
-    MPmap.find mp env.env_globals.env_modules
+    MPmap.find mp env.env_globals.Globals.modules
 
 
-let lookup_modtype mp env = 
-  MPmap.find mp env.env_globals.env_modtypes
+let lookup_modtype mp env =
+  MPmap.find mp env.env_globals.Globals.modtypes
 
 (*s Judgments. *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f7de98dcfb..5af2a7288b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -46,8 +46,18 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
-type globals
-(** globals = constants + projections + inductive types + modules + module-types *)
+module Globals : sig
+  type t
+
+  type view =
+    { constants : constant_key Cmap_env.t
+    ; inductives : mind_key Mindmap_env.t
+    ; modules : module_body MPmap.t
+    ; modtypes : module_type_body MPmap.t
+    }
+
+  val view : t -> view
+end
 
 type stratification = {
   env_universes : UGraph.t;
@@ -67,7 +77,7 @@ type rel_context_val = private {
 }
 
 type env = private {
-  env_globals       : globals;
+  env_globals       : Globals.t;
   env_named_context : named_context_val; (* section variables *)
   env_rel_context   : rel_context_val;
   env_nb_rel        : int;