Universe level maps use HMaps.

2 files changed, 14 insertions, 15 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 08a7e94544..fc060940cb 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -378,22 +378,9 @@ module Level = struct
 
 end
 
-module LSet = struct
-  module M = Set.Make (Level)
-  include M
-
-  let pr s = 
-    str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}"
-
-  let of_array l =
-    Array.fold_left (fun acc x -> add x acc) empty l
-
-end
-
-
 (** Level maps *)
 module LMap = struct 
-  module M = Map.Make (Level)
+  module M = HMap.Make (Level)
   include M
 
   let union l r = 
@@ -420,6 +407,18 @@ module LMap = struct
       Level.pr u ++ f v) (bindings m))
 end
 
+module LSet = struct
+  include LMap.Set
+
+  let pr s =
+    str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}"
+
+  let of_array l =
+    Array.fold_left (fun acc x -> add x acc) empty l
+
+end
+
+
 type 'a universe_map = 'a LMap.t
 
 type universe_level = Level.t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 25d25fa353..f9b8617c2e 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -44,7 +44,7 @@ type universe_level = Level.t
 (** Sets of universe levels *)
 module LSet : 
 sig 
-  include Set.S with type elt = universe_level
+  include CSig.SetS with type elt = universe_level
 	      
   val pr : t -> Pp.std_ppcmds
   (** Pretty-printing *)