package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 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.

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