Module UnivMinim

module UPairSet : CSet.S with type S.elt = Univ.Level.t * Univ.Level.t

Unordered pairs of universe levels (ie (u,v) = (v,u))

type extra = {
weak_constraints : UPairSet.t;
above_prop : Univ.Level.Set.t;
}
val empty_extra : extra
val extra_union : extra -> extra -> extra
val normalize_context_set : lbound:UGraph.Bound.t -> UGraph.t -> Univ.ContextSet.t -> UnivFlex.t -> extra -> UnivFlex.t Univ.in_universe_context_set