package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.2.tar.gz
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926

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