coq-core.kernel
Names.Label
btauto_plugin
byte_config
cc_plugin
coq-core.boot
coq-core.checklib
coq-core.clib
coq-core.config
coq-core.coqworkmgrapi
coq-core.debugger_support
coq-core.dev
coq-core.engine
coq-core.gramlib
coq-core.interp
coq-core.lib
coq-core.library
coq-core.parsing
coq-core.perf
coq-core.plugins
coq-core.pretyping
coq-core.printing
coq-core.proofs
coq-core.stm
coq-core.sysinit
coq-core.tactics
coq-core.toplevel
coq-core.vernac
coq-core.vm
derive_plugin
extraction_plugin
firstorder_plugin
funind_plugin
ltac2_ltac1_plugin
ltac2_plugin
ltac_plugin
micromega_core_plugin
micromega_plugin
nsatz_plugin
number_string_notation_plugin
ring_plugin
rtauto_plugin
ssreflect_plugin
ssrmatching_plugin
tauto_plugin
tuto0_plugin
tuto1_plugin
tuto2_plugin
tuto3_plugin
zify_plugin
type t
Type of labels
val equal : t -> t -> bool
Equality over labels
val compare : t -> t -> int
Comparison over labels.
val hash : t -> int
Hash over labels.
val make : string -> t
Create a label out of a string.
val of_id : Id.t -> t
Conversion from an identifier.
val to_id : t -> Id.t
Conversion to an identifier.
val to_string : t -> string
Conversion to string.
val print : t -> Pp.t
Pretty-printer.
module Set : Util.Set.S with type elt = t
module Map : Util.Map.ExtS with type key = t and module Set := Set
val hcons : t -> t