package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module CoqlibSource

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.

Sourceval lib_ref : string -> Names.GlobRef.t

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

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_ind_ref : string -> Names.inductive -> bool

Checks whether a name is bound to a known inductive.

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

List of all currently bound names.

For Equality tactics

Sourcetype 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;
}
Sourceval build_sigma_set : coq_sigma_data Util.delayed
Sourceval build_sigma_type : coq_sigma_data Util.delayed
Sourcetype 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;
}
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
Sourceval 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
Sourceval arith_modules : string list list
  • deprecated Please use Coqlib.lib_ref
Sourceval zarith_base_modules : string list list
  • deprecated Please use Coqlib.lib_ref
Sourceval init_modules : string list list
  • deprecated Please use Coqlib.lib_ref
Global references
Sourceval logic_module : Names.ModPath.t

Modules

  • deprecated Please use Coqlib.lib_ref
Sourceval logic_type_module : Names.DirPath.t
  • deprecated Please use Coqlib.lib_ref

Identity

  • deprecated Please use Coqlib.lib_ref
Sourceval type_of_id : Names.Constant.t
  • deprecated Please use Coqlib.lib_ref

Natural numbers

  • deprecated Please use Coqlib.lib_ref
Sourceval glob_nat : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
Sourceval path_of_O : Names.constructor
  • deprecated Please use Coqlib.lib_ref
Sourceval path_of_S : Names.constructor
  • deprecated Please use Coqlib.lib_ref
  • deprecated Please use Coqlib.lib_ref
  • deprecated Please use Coqlib.lib_ref
Sourceval glob_bool : Names.GlobRef.t

Booleans

  • deprecated Please use Coqlib.lib_ref
Sourceval path_of_true : Names.constructor
  • deprecated Please use Coqlib.lib_ref
Sourceval path_of_false : Names.constructor
  • deprecated Please use Coqlib.lib_ref
Sourceval glob_true : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
Sourceval glob_false : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
Sourceval glob_eq : Names.GlobRef.t

Equality

  • deprecated Please use Coqlib.lib_ref
Sourceval glob_identity : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
Sourceval glob_jmeq : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
...

Constructions and patterns related to Coq initial state are unknown at compile time. Therefore, we can only provide methods to build them at runtime. This is the purpose of the constr delayed and constr_pattern delayed types. Objects of this time needs to be forced with delayed_force to get the actual constr or pattern at runtime.

Sourcetype coq_bool_data = {
  1. andb : Names.GlobRef.t;
  2. andb_prop : Names.GlobRef.t;
  3. andb_true_intro : Names.GlobRef.t;
}
Sourceval build_bool_type : coq_bool_data Util.delayed
  • deprecated Please use Coqlib.lib_ref

Non-dependent pairs in Set from Datatypes

  • deprecated Please use Coqlib.lib_ref

= (build_coq_eq_data()).eq

  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_eq_refl : Names.GlobRef.t Util.delayed

= (build_coq_eq_data()).refl

  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_eq_sym : Names.GlobRef.t Util.delayed

= (build_coq_eq_data()).sym

  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_f_equal2 : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref

Data needed for discriminate and injection

Sourcetype coq_inversion_data = {
  1. inv_eq : Names.GlobRef.t;
    (*

    : forall params, args -> Prop

    *)
  2. inv_ind : Names.GlobRef.t;
    (*

    : forall params P (H : P params) args, eq params args -> P args

    *)
  3. inv_congr : Names.GlobRef.t;
    (*

    : forall params B (f:t->B) args, eq params args -> f params = f args

    *)
}
Sourceval build_coq_inversion_eq_data : coq_inversion_data Util.delayed
  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_inversion_identity_data : coq_inversion_data Util.delayed
  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_inversion_jmeq_data : coq_inversion_data Util.delayed
  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_inversion_eq_true_data : coq_inversion_data Util.delayed
  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_sumbool : Names.GlobRef.t Util.delayed

Specif

  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_False : Names.GlobRef.t Util.delayed

...

Connectives The False proposition

  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_True : Names.GlobRef.t Util.delayed

The True proposition and its unique proof

  • deprecated Please use Coqlib.lib_ref
  • deprecated Please use Coqlib.lib_ref

Negation

  • deprecated Please use Coqlib.lib_ref

Conjunction

  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_conj : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_iff_left_proj : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_iff_right_proj : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_prod : Names.GlobRef.t Util.delayed

Pairs

  • deprecated Please use Coqlib.lib_ref
Sourceval build_coq_pair : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref

Disjunction

  • deprecated Please use Coqlib.lib_ref

Existential quantifier

  • deprecated Please use Coqlib.lib_ref
Sourceval coq_eq_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_identity_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_jmeq_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_eq_true_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_existS_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_existT_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_exist_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_not_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_False_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_sumbool_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_sig_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_or_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
Sourceval coq_iff_ref : Names.GlobRef.t lazy_t
  • 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