package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val pr_with_global_universes : Univ.Level.t -> Pp.t
val qualid_of_level : Univ.Level.t -> Libnames.qualid
val add_global_universe : Univ.Level.t -> Decl_kinds.polymorphic -> unit
val is_polymorphic : Univ.Level.t -> bool
type universe_binders = Univ.Level.t Names.Id.Map.t
val empty_binders : universe_binders
val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
val universe_binders_of_global : Names.GlobRef.t -> universe_binders
type univ_name_list = Names.lname list
val universe_binders_with_opt_names : Names.GlobRef.t -> Univ.Level.t list -> univ_name_list option -> universe_binders