Using Hashmaps by default in constant and inductive maps. This changes fold and

iter order, but it seems nobody was relying on it (contrarily to the string case).

1 files changed, 2 insertions, 19 deletions

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index d6f0e7d1cd..964d709cff 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -25,26 +25,9 @@ type constant_key = constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
-module type Map =
-sig
-  type t
-  type key
-  type value
-  val empty : t
-  val add : key -> value -> t -> t
-  val find : key -> t -> value
-  val fold : (key -> value -> 'a -> 'a) -> t -> 'a -> 'a
-end
-
-module Constants : Map
-  with type key := Constant.t and type value := constant_key
-
-module Inductives : Map
-  with type key := MutInd.t and type value := mind_key
-
 type globals = {
-  env_constants : Constants.t;
-  env_inductives : Inductives.t;
+  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}