Module UnivNames

Local universe name <-> level mapping

val empty_binders : universe_binders
val empty_rev_binders : rev_binders
type univ_name_list = {
  1. qualities : Names.lname list;
  2. ext_ql : bool;
  3. univlevels : Names.lname list;
  4. ext_ul : bool;
}
val pr_level_with_global_universes : ?binders:universe_binders -> Univ.Level.t -> Pp.t
val qualid_of_level : universe_binders -> Univ.Level.t -> Libnames.qualid option
val pr_quality_with_global_universes : ?binders:universe_binders -> Sorts.Quality.t -> Pp.t
val qualid_of_quality : universe_binders -> Sorts.Quality.t -> Libnames.qualid option
val quality_printer : universe_binders -> Sorts.Quality.printer
val sort_printer : universe_binders -> Sorts.printer