From 3984f3c1db51f7b788ad49eafb7647774e8d1f53 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Mon, 18 Jun 2018 14:04:25 +0200
Subject: Make Environ.globals abstract.

---
 kernel/environ.ml     |  8 ++++++--
 kernel/environ.mli    | 14 ++++++--------
 kernel/safe_typing.ml |  2 +-
 3 files changed, 13 insertions(+), 11 deletions(-)

(limited to 'kernel')

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}
 
-- 
cgit v1.2.3