Module Names

This file defines a lot of different notions of names used pervasively in the kernel as well as in other places. The essential datatypes exported by this API are:

Identifiers
module Id : sig ... end

Representation and operations on identifiers.

module Name : sig ... end

Representation and operations on identifiers that are allowed to be anonymous (i.e. "_" in concrete syntax).

Type aliases
type name = Name.t =
  1. | Anonymous
  2. | Name of Id.t
  • deprecated (8.8) Use Name.t
type variable = Id.t
Directory paths = section names paths
module DirPath : sig ... end
module DPset = DirPath.Set
module DPmap = DirPath.Map
Unique names for bound modules
module MBId : sig ... end
module MBIset = MBId.Set
module MBImap = MBId.Map
The module part of the kernel name
module ModPath : sig ... end
module MPset = ModPath.Set
module MPmap = ModPath.Map
The absolute names of objects seen by kernel
module KerName : sig ... end
module KNset = KerName.Set
module KNpred = KerName.Pred
module KNmap = KerName.Map
Signature for quotiented names
module type EqType = sig ... end
module type QNameS = sig ... end
Constant Names
module Constant : sig ... end
module Cset : CSig.USetS with type elt = Constant.t

Sets and maps use the UserOrd ordering to index keys.

module Cmap : Util.Map.UExtS with type key = Constant.t and module Set := Cset
module Cpred : Predicate.S with type elt = Constant.t
module Cset_env = Cset
module Cmap_env = Cmap
Inductive names
module MutInd : sig ... end
module Mindset : CSig.USetS with type elt = MutInd.t
module Mindmap : Util.Map.UExtS with type key = MutInd.t and module Set := Mindset
module Mindmap_env = Mindmap
module Ind : sig ... end
type inductive = Ind.t
module Construct : sig ... end
type constructor = Construct.t
module Indset : CSet.ExtS with type elt = inductive
module Constrset : CSet.ExtS with type elt = constructor
module Indmap : CMap.ExtS with type key = inductive and module Set := Indset
module Constrmap : CMap.ExtS with type key = constructor and module Set := Constrset
module Indset_env = Indset
module Constrset_env = Constrset
module Indmap_env = Indmap
module Constrmap_env = Constrmap
val ith_mutual_inductive : inductive -> int -> inductive
val ith_constructor_of_inductive : inductive -> int -> constructor
val inductive_of_constructor : constructor -> inductive
val index_of_constructor : constructor -> int
Hash-consing
val hcons_con : Constant.t Hashcons.f
val hcons_mind : MutInd.t Hashcons.f
val hcons_ind : inductive Hashcons.f
val hcons_construct : constructor Hashcons.f
type 'a tableKey =
  1. | ConstKey of 'a
  2. | VarKey of Id.t
  3. | RelKey of Int.t
type inv_rel_key = int

index in the rel_context part of environment starting by the end, inverse of de Bruijn indice

val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool
val hash_table_key : ('a -> int) -> 'a tableKey -> int
val eq_constant_key : Constant.t -> Constant.t -> bool
Module paths
type module_path = ModPath.t =
  1. | MPfile of DirPath.t
  2. | MPbound of MBId.t
  3. | MPdot of ModPath.t * Id.t
  • deprecated (8.8) Alias type
module Projection : sig ... end
module PRset : CSig.USetS with type elt = Projection.Repr.t
module PRmap : Util.Map.UExtS with type key = Projection.Repr.t and module Set := PRset
module PRset_env = PRset
module PRmap_env = PRmap
Global reference is a kernel side type for all references together
module GlobRef : sig ... end

Located identifiers and objects with syntax.

type lident = Id.t CAst.t
type lname = Name.t CAst.t
type lstring = string CAst.t
val lident_eq : lident -> lident -> bool
module Label : sig ... end

Deprecated