From 00df486efd76070b6c3673071050565e0ed4466e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Mar 2014 21:39:39 +0100
Subject: Using HMaps in Safe_env.environments, hopefully improving
 performances.

---
 kernel/pre_env.mli | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'kernel/pre_env.mli')

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