Module Names.GlobRef

type t =
| VarRef of variable(*

A reference to the section-context.

*)
| ConstRef of Constant.t(*

A reference to the environment.

*)
| IndRef of inductive(*

A reference to an inductive type.

*)
| ConstructRef of constructor(*

A reference to a constructor of an inductive type.

*)
val equal : t -> t -> bool
val is_bound : t -> bool
include QNameS with type t := t
module CanOrd : EqType with type t = t

Equality functions over the canonical name. Their use should be restricted to the kernel.

module UserOrd : EqType with type t = t

Equality functions over the user name.

module SyntacticOrd : EqType with type t = t

Equality functions using both names, for low-level uses.

module Set_env : CSig.SetS with type elt = t
module Map_env : Util.Map.ExtS with type key = t and module Set := Set_env
module Set : CSig.SetS with type elt = t
module Map : Util.Map.ExtS with type key = t and module Set := Set
val print : t -> Pp.t

Print internal representation (not to be used for user-facing messages).