diff options
Diffstat (limited to 'kernel/uGraph.mli')
| -rw-r--r-- | kernel/uGraph.mli | 10 |
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]. *) |