Module UnivNames
type universe_binders= Univ.Level.t Names.Id.Map.t
val empty_binders : universe_binders
type univ_name_list= Names.lname list
val pr_with_global_universes : universe_binders -> Univ.Level.t -> Pp.tval qualid_of_level : universe_binders -> Univ.Level.t -> Libnames.qualid option