Make Environ.globals abstract.

5 files changed, 20 insertions, 20 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 811abd67f..ab679a71c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -232,7 +232,7 @@ let ppenv e = pp
 let ppenvwithcst e = pp
   (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
-   str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).env_globals.env_constants (mt ()) ++ str "}")
+   str "{" ++ Environ.fold_constants (fun a _ s -> Constant.print a ++ spc () ++ s) e (mt ()) ++ str "}")
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 0e34a7165..224b6d5b8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -55,7 +55,8 @@ type globals = {
   env_projections : projection_body Cmap_env.t;
   env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body MPmap.t}
+  env_modtypes : module_type_body MPmap.t;
+}
 
 type stratification = {
   env_universes : UGraph.t;
@@ -86,7 +87,7 @@ type rel_context_val = {
 }
 
 type env = {
-  env_globals       : globals;           (* globals = constants + inductive types + modules + module-types *)
+  env_globals       : globals;
   env_named_context : named_context_val; (* section variables *)
   env_rel_context   : rel_context_val;
   env_nb_rel        : int;
@@ -208,6 +209,9 @@ let lookup_named_val id env =
 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
+
 (* Global constants *)
 
 let lookup_constant_key kn env =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8928b32f1..4c637bf78 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -46,13 +46,8 @@ type constant_key = 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_projections : projection_body Cmap_env.t;
-  env_inductives : mind_key Mindmap_env.t;
-  env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body MPmap.t
-}
+type globals
+(** globals = constants + projections + inductive types + modules + module-types *)
 
 type stratification = {
   env_universes : UGraph.t;
@@ -70,7 +65,7 @@ type rel_context_val = private {
 }
 
 type env = private {
-  env_globals       : globals;           (* globals = constants + inductive types + modules + module-types *)
+  env_globals       : globals;
   env_named_context : named_context_val; (* section variables *)
   env_rel_context   : rel_context_val;
   env_nb_rel        : int;
@@ -175,6 +170,9 @@ val reset_with_named_context : named_context_val -> env -> env
 (** This removes the [n] last declarations from the rel context *)
 val pop_rel_context : int -> env -> env
 
+(** Useful for printing *)
+val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a
+
 (** {5 Global constants }
   {6 Add entries to global environment } *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 12c82e20d..caa935506 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -918,7 +918,7 @@ let register_inline kn senv =
   if not (evaluable_constant kn senv.env) then
     CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected");
   let env = senv.env in
-  let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in
+  let cb = lookup_constant kn env in
   let cb = {cb with const_inline_code = true} in
   let env = add_constant kn cb env in { senv with env}
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 43c974846..6d1abeca1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -263,15 +263,13 @@ let print_namespace ns =
   let matches mp = match match_modulepath ns mp with
   | Some [] -> true
   | _ -> false in
-  let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in
   let constants_in_namespace =
-    Cmap_env.fold (fun c (body,_) acc ->
-      let kn = Constant.user c in
-      if matches (KerName.modpath kn) then
-        acc++fnl()++hov 2 (print_constant kn body)
-      else
-        acc
-    ) constants (str"")
+    Environ.fold_constants (fun c body acc ->
+        let kn = Constant.user c in
+        if matches (KerName.modpath kn)
+        then acc++fnl()++hov 2 (print_constant kn body)
+        else acc)
+      (Global.env ()) (str"")
   in
   (print_list Id.print ns)++str":"++fnl()++constants_in_namespace