package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

doc/coq-core.kernel/Names/GlobRef/index.html

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

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

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