val pp_constraints: unit -> string
val get_universes: unit -> NCic.universe list
-(* The type of Prop, smaller than any other type *)
-val type0: NCic.universe
-
(* use to type products *)
val max: NCic.universe -> NCic.universe -> NCic.universe
val add_lt_constraint: NCic.universe -> NCic.universe -> unit
val universe_eq: NCic.universe -> NCic.universe -> bool
val universe_leq: NCic.universe -> NCic.universe -> bool
+val universe_lt: NCic.universe -> NCic.universe -> bool
(* checks if s1 <= s2 *)
val are_sorts_convertible: test_eq_only:bool -> NCic.sort -> NCic.sort -> bool
(* looks for a declared universe that is the least one above the input *)
val sup : NCic.universe -> NCic.universe option
+val inf : strict:bool -> NCic.universe -> NCic.universe option
+val family_of : NCic.universe -> [ `CProp | `Type ]
(* =========== /universes ============= *)