Module Univ

module UGlobal : sig ... end

Qualified global universe level

module Level : sig ... end

Universes.

module Universe : sig ... end

univ_level_mem l u Is l is mentioned in u ?

val univ_level_mem : Level.t -> Universe.t -> bool

univ_level_rem u v min removes u from v, resulting in min if v was exactly u.

val univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t
UnivConstraints.
module UnivConstraint : sig ... end
module UnivConstraints : sig ... end
type 'a constraint_function = 'a -> 'a -> UnivConstraints.t -> UnivConstraints.t

Enforcing UnivConstraints.t.

val enforce_eq_level : Level.t constraint_function
val enforce_leq_level : Level.t constraint_function