Inductive maps in Environ now use HMap.

4 files changed, 51 insertions, 22 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 0bf3923e4..a25714d77 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -206,7 +206,7 @@ let evaluable_constant cst env =
 let lookup_mind = lookup_mind
 
 let add_mind_key kn mind_key env =
-  let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
+  let new_inds = Inductives.add kn mind_key env.env_globals.env_inductives in
   let new_globals =
     { env.env_globals with
 	env_inductives = new_inds } in
diff --git a/kernel/names.mli b/kernel/names.mli
index 3b7de68d9..4b71766bb 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -363,11 +363,13 @@ sig
   module CanOrd : sig
     val compare : t -> t -> int
     val equal : t -> t -> bool
+    val hash : t -> int
   end
 
   module UserOrd : sig
     val compare : t -> t -> int
     val equal : t -> t -> bool
+    val hash : t -> int
   end
 
   val equal : t -> t -> bool
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 3509ccf0c..f584edc3b 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -38,24 +38,43 @@ type constant_key = constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
-module Constants =
+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 M =
-  struct
-    type t = Constant.t
-    include Constant.UserOrd
-  end
-  module CMap = HMap.Make(M)
-  type t = constant_key CMap.t
-  let empty = CMap.empty
-  let add = CMap.add
-  let find = CMap.find
-  let fold = CMap.fold
+  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 : mind_key Mindmap_env.t;
+  env_inductives : Inductives.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 
@@ -97,7 +116,7 @@ let empty_named_context_val = [],[]
 let empty_env = {
   env_globals = {
     env_constants = Constants.empty;
-    env_inductives = Mindmap_env.empty;
+    env_inductives = Inductives.empty;
     env_modules = MPmap.empty;
     env_modtypes = MPmap.empty};
   env_named_context = empty_named_context;
@@ -172,7 +191,7 @@ let lookup_constant kn env =
 
 (* Mutual Inductives *)
 let lookup_mind kn env =
-  fst (Mindmap_env.find kn env.env_globals.env_inductives)
+  fst (Inductives.find kn env.env_globals.env_inductives)
 
 let lookup_mind_key kn env =
-  Mindmap_env.find kn env.env_globals.env_inductives
+  Inductives.find kn env.env_globals.env_inductives
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 4596b23aa..d6f0e7d1c 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -25,18 +25,26 @@ type constant_key = constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
-module Constants :
+module type Map =
 sig
   type t
+  type key
+  type value
   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
+  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 : mind_key Mindmap_env.t;
+  env_inductives : Inductives.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}