From 3007da7147d86f2e85347b9e70c1faea7d2eed06 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Jul 2014 19:42:44 +0200
Subject: Universe level maps use HMaps.

---
 kernel/univ.ml  | 27 +++++++++++++--------------
 kernel/univ.mli |  2 +-
 2 files changed, 14 insertions(+), 15 deletions(-)

(limited to 'kernel')

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