Make explicit that UGraph lower bounds are only of two kinds.

This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.

1 files changed, 8 insertions, 2 deletions

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8d9afb0990..c9fbd7f694 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -48,7 +48,13 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
 
 exception AlreadyDeclared
 
-val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t
+module Bound :
+sig
+  type t = Prop | Set
+  (** The [Prop] bound is only used for template polymorphic inductive types. *)
+end
+
+val add_universe : Level.t -> lbound:Bound.t -> strict:bool -> t -> t
 
 (** Add a universe without (Prop,Set) <= u *)
 val add_universe_unconstrained : Level.t -> t -> t
@@ -86,7 +92,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t
 val domain : t -> LSet.t
 (** Known universes *)
 
-val check_subtype : lbound:Level.t -> AUContext.t check_function
+val check_subtype : lbound:Bound.t -> AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)