package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type univ_unique_id
val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer
val new_univ_id : unit -> univ_unique_id
val new_univ_global : unit -> Univ.Level.UGlobal.t
val fresh_level : unit -> Univ.Level.t
val new_global_univ : unit -> Univ.Universe.t Univ.in_universe_context_set
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_monomorphic_global : Names.GlobRef.t -> Constr.constr