package coq

  1. Overview
  2. Docs

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

Sourcemodule Set_env : CSig.SetS with type elt = t
Sourcemodule Map_env : Util.Map.ExtS with type key = t and module Set := Set_env
Sourcemodule Set : CSig.SetS with type elt = t
Sourcemodule Map : Util.Map.ExtS with type key = t and module Set := Set