package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type universe_id = Names.DirPath.t * int
val set_remote_new_univ_id : universe_id RemoteCounter.installer
val new_univ_id : unit -> universe_id
val new_univ_level : unit -> Univ.Level.t
val new_univ : unit -> Univ.Universe.t
val new_Type : unit -> Constr.types
val new_Type_sort : unit -> Sorts.t
val new_global_univ : unit -> Univ.Universe.t Univ.in_universe_context_set
val new_sort_in_family : Sorts.family -> Sorts.t
val fresh_instance_from_context : Univ.AUContext.t -> Univ.Instance.t Univ.constrained
val fresh_sort_in_family : Sorts.family -> Sorts.t Univ.in_universe_context_set
val fresh_universe_context_set_instance : Univ.ContextSet.t -> Univ.universe_level_subst * Univ.ContextSet.t
val constr_of_global_univ : Names.GlobRef.t Univ.puniverses -> Constr.constr
val constr_of_global : Names.GlobRef.t -> Constr.constr