Names (coq-core.Names)

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 =

| Anonymous

| Name of Id.t

type variable = Id.t

type module_ident = Id.t

module ModIdset : Util.Set.ExtS with type elt = module_ident

module ModIdmap : Util.Map.ExtS with type key = module_ident and module Set := ModIdset

Directory paths = section names paths

module DirPath : sig ... end

module DPset : Util.Set.ExtS with type elt = DirPath.t

module DPmap : Util.Map.ExtS with type key = DirPath.t and module Set := DPset

Names of structure elements

module Label : sig ... end

Unique names for bound modules

module MBId : sig ... end

module MBIset : Util.Set.ExtS with type elt = MBId.t

module MBImap : Util.Map.ExtS with type key = MBId.t and module Set := MBIset

The module part of the kernel name

module ModPath : sig ... end

module MPset : Util.Set.ExtS with type elt = ModPath.t

module MPmap : Util.Map.ExtS with type key = ModPath.t and module Set := MPset

The absolute names of objects seen by kernel

module KerName : sig ... end

module KNset : CSig.USetS with type elt = KerName.t

module KNpred : Predicate.S with type elt = KerName.t

module KNmap : Util.Map.UExtS with type key = KerName.t and module Set := KNset

Signature for quotiented names

module type EqType = sig ... end

module type QNameS = sig ... end

Constant Names

module Constant : sig ... end

module Cpred : Predicate.S with type elt = Constant.t

The *_env modules consider an order on user part of names the others consider an order on canonical part of names

module Cset : CSig.USetS with type elt = Constant.t

module Cset_env : CSig.USetS with type elt = Constant.t

module Cmap : Util.Map.UExtS with type key = Constant.t and module Set := Cset

A map whose keys are constants (values of the Constant.t type). Keys are ordered wrt. "canonical form" of the constant.

module Cmap_env : Util.Map.UExtS with type key = Constant.t and module Set := Cset_env

A map whose keys are constants (values of the Constant.t type). Keys are ordered wrt. "user form" of the constant.

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 : CMap.UExtS with type key = MutInd.t

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 Indset_env : CSet.ExtS with type elt = inductive

module Constrset_env : 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 Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset_env

module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env

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 -> Constant.t

val hcons_mind : MutInd.t -> MutInd.t

val hcons_ind : inductive -> inductive

val hcons_construct : constructor -> constructor

type 'a tableKey =

| ConstKey of 'a

| VarKey of Id.t

| 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

equalities on constant and inductive names (for the checker)

val eq_ind_chk : inductive -> inductive -> bool

Module paths

type module_path = ModPath.t =

| MPfile of DirPath.t

| MPbound of MBId.t

| MPdot of ModPath.t * Label.t

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 PRpred : Predicate.S with type elt = Projection.Repr.t

Predicate on projection representation (ignoring unfolding state)

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