2 files changed, 21 insertions, 4 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index e31e2be68..660e39e63 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -54,6 +54,11 @@ module UniverseLevel = struct
 end
 
 module UniverseLMap = Map.Make (UniverseLevel)
+module UniverseLSet = Set.Make (UniverseLevel)
+
+type universe_level = UniverseLevel.t
+
+let compare_levels = UniverseLevel.compare
 
 (* An algebraic universe [universe] is either a universe variable
    [UniverseLevel.t] or a formal universe known to be greater than some
@@ -71,7 +76,13 @@ type universe =
   | Atom of UniverseLevel.t
   | Max of UniverseLevel.t list * UniverseLevel.t list
 
-let make_univ (m,n) = Atom (UniverseLevel.Level (m,n))
+let make_universe_level (m,n) = UniverseLevel.Level (m,n)
+let make_universe l = Atom l
+let make_univ c = Atom (make_universe_level c)
+
+let universe_level = function
+  | Atom l -> Some l
+  | Max _ -> None
 
 let pr_uni_level u = str (UniverseLevel.to_string u)
 
@@ -500,9 +511,6 @@ let merge_constraints c g =
 
 (* Normalization *)
 
-module UniverseLSet =
- Set.Make (UniverseLevel)
-
 let lookup_level u g =
   try Some (UniverseLMap.find u g) with Not_found -> None
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e19a4c43a..2f99e16ec 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -8,8 +8,11 @@
 
 (** Universes. *)
 
+type universe_level
 type universe
 
+module UniverseLSet : Set.S with type elt = universe_level
+
 (** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... 
    Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
 
@@ -17,12 +20,17 @@ val type0m_univ : universe  (** image of Prop in the universes hierarchy *)
 val type0_univ : universe  (** image of Set in the universes hierarchy *)
 val type1_univ : universe  (** the universe of the type of Prop/Set *)
 
+val make_universe_level : Names.dir_path * int -> universe_level
+val make_universe : universe_level -> universe
 val make_univ : Names.dir_path * int -> universe
 
 val is_type0_univ : universe -> bool
 val is_type0m_univ : universe -> bool
 val is_univ_variable : universe -> bool
 
+val universe_level : universe -> universe_level option
+val compare_levels : universe_level -> universe_level -> int
+
 (** The type of a universe *)
 val super : universe -> universe
 
@@ -82,6 +90,7 @@ val no_upper_constraints : universe -> constraints -> bool
 
 (** {6 Pretty-printing of universes. } *)
 
+val pr_uni_level : universe_level -> Pp.std_ppcmds
 val pr_uni : universe -> Pp.std_ppcmds
 val pr_universes : universes -> Pp.std_ppcmds
 val pr_constraints : constraints -> Pp.std_ppcmds