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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct