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, 3 insertions, 3 deletions

diff --git a/engine/uState.mli b/engine/uState.mli
index 6707826aae..533a501b59 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -25,9 +25,9 @@ type t
 
 val empty : t
 
-val make : lbound:Univ.Level.t -> UGraph.t -> t
+val make : lbound:UGraph.Bound.t -> UGraph.t -> t
 
-val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t
+val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
 
 val is_empty : t -> bool
 
@@ -90,7 +90,7 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
    the universes in [keep]. The constraints [csts] are adjusted so
    that transitive constraints between remaining universes (those in
    [keep] and those not in [univs]) are preserved. *)
-val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:UGraph.Bound.t -> ContextSet.t -> LSet.t -> ContextSet.t
 
 (** [restrict uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by local named universes and side effect universes