Module `Coqlib`Source

Indirection between logical names and global references.

This module provides a mechanism to bind “names” to constants and to look up these constants using their names.

The two main functions are register_ref n r which binds the name n to the reference r and lib_ref n which returns the previously registered reference under name n.

The first function is meant to be available through the vernacular command Register r as n, so that plug-ins can refer to a constant without knowing its user-facing name, the precise module path in which it is defined, etc.

For instance, lib_ref "core.eq.type" returns the proper GlobRef.t for the type of the core equality type.

Sourceval register_ref : string -> Names.GlobRef.t -> unit

Registers a global reference under the given name.

Sourceexception NotFoundRef of string

Sourceval lib_ref : string -> Names.GlobRef.t

Retrieves the reference bound to the given name (by a previous call to register_ref). Raises NotFoundRef if no reference is bound to this name.

Sourceval lib_ref_opt : string -> Names.GlobRef.t option

As lib_ref but returns None instead of raising.

Sourceval has_ref : string -> bool

Checks whether a name refers to a registered constant. For any name n, if has_ref n returns true, lib_ref n will succeed.

Sourceval check_ref : string -> Names.GlobRef.t -> bool

Checks whether a name is bound to a known reference.

Sourceval check_ind_ref : string -> Names.inductive -> bool

Checks whether a name is bound to a known inductive.

deprecated Use Coqlib.check_ref

Sourceval get_lib_refs : unit -> (string * Names.GlobRef.t) list

List of all currently bound names.

For Equality tactics

Sourcetype coq_sigma_data = {

proj1 : Names.GlobRef.t;
proj2 : Names.GlobRef.t;
elim : Names.GlobRef.t;
intro : Names.GlobRef.t;
typ : Names.GlobRef.t;

}

Sourceval build_sigma_type : coq_sigma_data Util.delayed

Sourceval build_sigma : coq_sigma_data Util.delayed

Sourceval build_prod : coq_sigma_data Util.delayed

Sourcetype coq_eq_data = {

eq : Names.GlobRef.t;
ind : Names.GlobRef.t;
refl : Names.GlobRef.t;
sym : Names.GlobRef.t;
trans : Names.GlobRef.t;
congr : Names.GlobRef.t;

}

Sourceval build_coq_eq_data : coq_eq_data Util.delayed

Sourceval build_coq_identity_data : coq_eq_data Util.delayed

Sourceval build_coq_jmeq_data : coq_eq_data Util.delayed

Sourceval check_required_library : string list -> unit

For tactics/commands requiring vernacular libraries

Sourceval datatypes_module_name : string list

Sourceval logic_module_name : string list

Sourceval jmeq_module_name : string list

DEPRECATED

All the functions below are deprecated and should go away in the next coq version ...

Sourceval find_reference : string -> string list -> string -> Names.GlobRef.t

find_reference caller_message [dir;subdir;...] s returns a global reference to the name dir.subdir.(...).s; the corresponding module must have been required or in the process of being compiled so that it must be used lazily; it raises an anomaly with the given message if not found

deprecated Please use Coqlib.lib_ref

Sourceval coq_reference : string -> string list -> string -> Names.GlobRef.t

This just prefixes find_reference with Coq...

deprecated Please use Coqlib.lib_ref

Source

val gen_reference_in_modules : 
  string ->
  string list list ->
  string ->
  Names.GlobRef.t

Search in several modules (not prefixed by "Coq")

deprecated Please use Coqlib.lib_ref

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Coqlib/index.html

Module `Coqlib`Source

For Equality tactics

DEPRECATED

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Coqlib/index.html

Module CoqlibSource

For Equality tactics

DEPRECATED

Module `Coqlib`Source