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, 8 insertions, 42 deletions

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index f584edc3b0..b655887d70 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -38,43 +38,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 Make(M : sig include HMap.HashedType type value end) =
-struct
-  module Map = HMap.Make(M)
-  type t = M.value Map.t
-  let empty = Map.empty
-  let add = Map.add
-  let find = Map.find
-  let fold = Map.fold
-end
-
-module Constants = Make(struct
-  type t = Constant.t
-  type value = constant_key
-  include Constant.UserOrd
-end)
-
-module Inductives = Make(struct
-  type t = MutInd.t
-  type value = mind_key
-  include MutInd.UserOrd
-end)
-
-
 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}
 
@@ -115,8 +81,8 @@ let empty_named_context_val = [],[]
 
 let empty_env = {
   env_globals = {
-    env_constants = Constants.empty;
-    env_inductives = Inductives.empty;
+    env_constants = Cmap_env.empty;
+    env_inductives = Mindmap_env.empty;
     env_modules = MPmap.empty;
     env_modtypes = MPmap.empty};
   env_named_context = empty_named_context;
@@ -184,14 +150,14 @@ let env_of_named id env = env
 (* Global constants *)
 
 let lookup_constant_key kn env =
-  Constants.find kn env.env_globals.env_constants
+  Cmap_env.find kn env.env_globals.env_constants
 
 let lookup_constant kn env =
-  fst (Constants.find kn env.env_globals.env_constants)
+  fst (Cmap_env.find kn env.env_globals.env_constants)
 
 (* Mutual Inductives *)
 let lookup_mind kn env =
-  fst (Inductives.find kn env.env_globals.env_inductives)
+  fst (Mindmap_env.find kn env.env_globals.env_inductives)
 
 let lookup_mind_key kn env =
-  Inductives.find kn env.env_globals.env_inductives
+  Mindmap_env.find kn env.env_globals.env_inductives