Using HMaps in Safe_env.environments, hopefully improving performances.

1 files changed, 10 insertions, 1 deletions

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 964d709cff..4596b23aaa 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -25,8 +25,17 @@ type constant_key = constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
+module Constants :
+sig
+  type t
+  val empty : t
+  val add : Constant.t -> constant_key -> t -> t
+  val find : Constant.t -> t -> constant_key
+  val fold : (Constant.t -> constant_key -> 'a -> 'a) -> t -> 'a  -> 'a
+end
+
 type globals = {
-  env_constants : constant_key Cmap_env.t;
+  env_constants : Constants.t;
   env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}