Module Names.GlobRefSource

Sourcetype t =
  1. | VarRef of variable
    (*

    A reference to the section-context.

    *)
  2. | ConstRef of Constant.t
    (*

    A reference to the environment.

    *)
  3. | IndRef of inductive
    (*

    A reference to an inductive type.

    *)
  4. | ConstructRef of constructor
    (*

    A reference to a constructor of an inductive type.

    *)
Sourceval equal : t -> t -> bool
  • deprecated (8.18) Use QGlobRef.equal
Sourceval is_bound : t -> bool
include QNameS with type t := t
Sourcemodule CanOrd : EqType with type t = t

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

Sourcemodule UserOrd : EqType with type t = t

Equality functions over the user name.

Sourcemodule SyntacticOrd : EqType with type t = t

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

Sourceval canonize : t -> t

Returns the canonical version of the name

module Set_env : CSig.USetS with type elt = t
Sourcemodule Map_env : Util.Map.UExtS with type key = t and module Set := Set_env
module Set : CSig.USetS with type elt = t
Sourcemodule Map : Util.Map.UExtS with type key = t and module Set := Set
Sourceval print : t -> Pp.t

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