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 -> UnivSubst.universe_opt_subst -> Univ.Level.Set.t -> extra -> (UnivSubst.universe_opt_subst * Univ.Level.Set.t) Univ.in_universe_context_set