Module `Univops`

val universes_of_constr : Constr.constr -> Univ.LSet.t: Return the set of all universes appearing in constr.

val restrict_universe_context : lbound:Univ.Level.t -> Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t