Module `UnivNames`

val pr_with_global_universes : Univ.Level.t -> Pp.t
val qualid_of_level : Univ.Level.t -> Libnames.qualid option

type universe_binders = Univ.Level.t Names.Id.Map.t

val empty_binders : universe_binders
val compute_instance_binders : Univ.Instance.t -> universe_binders -> Names.Name.t array

type univ_name_list = Names.lname list

val universe_binders_with_opt_names : Univ.AUContext.t -> univ_name_list option -> universe_binders

universe_binders_with_opt_names ref l

If l is Some univs return the universe binders naming the bound levels of ref by univs (skipping Anonymous). May error if the lengths mismatch.

Otherwise return the bound universe names registered for ref.