package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

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

Registers a global reference under the given name.

exception NotFoundRef of string
val 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.

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

As lib_ref but returns None instead of raising.

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

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

Checks whether a name is bound to a known reference.

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

Checks whether a name is bound to a known inductive.

  • deprecated Use Coqlib.check_ref
val get_lib_refs : unit -> (string * Names.GlobRef.t) list

List of all currently bound names.

For Equality tactics

type coq_sigma_data = {
  1. proj1 : Names.GlobRef.t;
  2. proj2 : Names.GlobRef.t;
  3. elim : Names.GlobRef.t;
  4. intro : Names.GlobRef.t;
  5. typ : Names.GlobRef.t;
}
val build_sigma_type : coq_sigma_data Util.delayed
val build_sigma : coq_sigma_data Util.delayed
val build_prod : coq_sigma_data Util.delayed
type coq_eq_data = {
  1. eq : Names.GlobRef.t;
  2. ind : Names.GlobRef.t;
  3. refl : Names.GlobRef.t;
  4. sym : Names.GlobRef.t;
  5. trans : Names.GlobRef.t;
  6. congr : Names.GlobRef.t;
}
val build_coq_eq_data : coq_eq_data Util.delayed
val build_coq_identity_data : coq_eq_data Util.delayed
val build_coq_jmeq_data : coq_eq_data Util.delayed
val check_required_library : string list -> unit

For tactics/commands requiring vernacular libraries

val datatypes_module_name : string list
val logic_module_name : string list
val jmeq_module_name : string list

DEPRECATED

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

val 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
val coq_reference : string -> string list -> string -> Names.GlobRef.t

This just prefixes find_reference with Coq...

  • deprecated Please use Coqlib.lib_ref
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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct