Imported Upstream version 8.5~beta3+dfsg

1 files changed, 18 insertions, 3 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7aaf2ffe..c926c57b 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -20,7 +20,11 @@ sig
 
   val is_small : t -> bool
   (** Is the universe set or prop? *)
-
+		       
+  val is_prop : t -> bool
+  val is_set : t -> bool
+  (** Is it specifically Prop or Set *)
+		       
   val compare : t -> t -> int
   (** Comparison function *)
 
@@ -87,6 +91,9 @@ sig
   val is_level : t -> bool
   (** Test if the universe is a level or an algebraic universe. *)
 
+  val is_levels : t -> bool
+  (** Test if the universe is a lub of levels or contains +n's. *)
+
   val level : t -> Level.t option
   (** Try to get a level out of a universe, returns [None] if it
       is an algebraic universe. *)
@@ -159,8 +166,12 @@ val is_initial_universes : universes -> bool
 
 val sort_universes : universes -> universes
 
-(** Adds a universe to the graph, ensuring it is >= Prop. *)
-val add_universe : universe_level -> universes -> universes
+(** Adds a universe to the graph, ensuring it is >= or > Set.
+   @raises AlreadyDeclared if the level is already declared in the graph. *)
+
+exception AlreadyDeclared
+
+val add_universe : universe_level -> bool -> universes -> universes
 
 (** {6 Constraints. } *)
 
@@ -332,6 +343,9 @@ sig
   (** Keeps the order of the instances *)
   val union : t -> t -> t
 
+  (* the number of universes in the context *)
+  val size : t -> int
+
 end
 
 type universe_context = UContext.t
@@ -349,6 +363,7 @@ sig
   val of_instance : Instance.t -> t
   val of_set : universe_set -> t
 
+  val equal : t -> t -> bool
   val union : t -> t -> t
 
   val append : t -> t -> t