Module Coqlib

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

Checks whether a name is bound to a known inductive.

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

List of all currently bound names.

For Equality tactics

type coq_sigma_data = {
proj1 : Names.GlobRef.t;
proj2 : Names.GlobRef.t;
elim : Names.GlobRef.t;
intro : Names.GlobRef.t;
typ : Names.GlobRef.t;
}
val build_sigma_set : coq_sigma_data Util.delayed
val build_sigma_type : coq_sigma_data Util.delayed
val build_sigma : coq_sigma_data Util.delayed
type 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;
}
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

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

This just prefixes find_reference with Coq...

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

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

val arith_modules : string list list
val zarith_base_modules : string list list
val init_modules : string list list
Global references
val logic_module : Names.ModPath.t

Modules

val logic_type_module : Names.DirPath.t

Identity

val type_of_id : Names.Constant.t

Natural numbers

val nat_path : Libnames.full_path
val glob_nat : Names.GlobRef.t
val path_of_O : Names.constructor
val path_of_S : Names.constructor
val glob_O : Names.GlobRef.t
val glob_S : Names.GlobRef.t
val glob_bool : Names.GlobRef.t

Booleans

val path_of_true : Names.constructor
val path_of_false : Names.constructor
val glob_true : Names.GlobRef.t
val glob_false : Names.GlobRef.t
val glob_eq : Names.GlobRef.t

Equality

val glob_identity : Names.GlobRef.t
val glob_jmeq : Names.GlobRef.t
...

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.

type coq_bool_data = {
andb : Names.GlobRef.t;
andb_prop : Names.GlobRef.t;
andb_true_intro : Names.GlobRef.t;
}
val build_bool_type : coq_bool_data Util.delayed
val build_prod : coq_sigma_data Util.delayed

Non-dependent pairs in Set from Datatypes

val build_coq_eq : Names.GlobRef.t Util.delayed

= (build_coq_eq_data()).eq

val build_coq_eq_refl : Names.GlobRef.t Util.delayed

= (build_coq_eq_data()).refl

val build_coq_eq_sym : Names.GlobRef.t Util.delayed

= (build_coq_eq_data()).sym

val build_coq_f_equal2 : Names.GlobRef.t Util.delayed

Data needed for discriminate and injection

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

: forall params, args -> Prop

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

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

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

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

*)
}
val build_coq_inversion_eq_data : coq_inversion_data Util.delayed
val build_coq_inversion_identity_data : coq_inversion_data Util.delayed
val build_coq_inversion_jmeq_data : coq_inversion_data Util.delayed
val build_coq_inversion_eq_true_data : coq_inversion_data Util.delayed
val build_coq_sumbool : Names.GlobRef.t Util.delayed

Specif

val build_coq_False : Names.GlobRef.t Util.delayed

...

Connectives The False proposition

val build_coq_True : Names.GlobRef.t Util.delayed

The True proposition and its unique proof

val build_coq_I : Names.GlobRef.t Util.delayed
val build_coq_not : Names.GlobRef.t Util.delayed

Negation

val build_coq_and : Names.GlobRef.t Util.delayed

Conjunction

val build_coq_conj : Names.GlobRef.t Util.delayed
val build_coq_iff : Names.GlobRef.t Util.delayed
val build_coq_iff_left_proj : Names.GlobRef.t Util.delayed
val build_coq_iff_right_proj : Names.GlobRef.t Util.delayed
val build_coq_prod : Names.GlobRef.t Util.delayed

Pairs

val build_coq_pair : Names.GlobRef.t Util.delayed
val build_coq_or : Names.GlobRef.t Util.delayed

Disjunction

val build_coq_ex : Names.GlobRef.t Util.delayed

Existential quantifier

val coq_eq_ref : Names.GlobRef.t lazy_t
val coq_identity_ref : Names.GlobRef.t lazy_t
val coq_jmeq_ref : Names.GlobRef.t lazy_t
val coq_eq_true_ref : Names.GlobRef.t lazy_t
val coq_existS_ref : Names.GlobRef.t lazy_t
val coq_existT_ref : Names.GlobRef.t lazy_t
val coq_exist_ref : Names.GlobRef.t lazy_t
val coq_not_ref : Names.GlobRef.t lazy_t
val coq_False_ref : Names.GlobRef.t lazy_t
val coq_sumbool_ref : Names.GlobRef.t lazy_t
val coq_sig_ref : Names.GlobRef.t lazy_t
val coq_or_ref : Names.GlobRef.t lazy_t
val coq_iff_ref : Names.GlobRef.t lazy_t