Module UnivMinim

module UPairSet : CSet.S with type 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

Simplification and pruning of constraints: normalize_context_set ctx us

val get_set_minimization : unit -> bool