Module Coqlib

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

Registers a global reference under the given name.

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

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

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
val id : Names.Constant.t

Identity

val type_of_id : Names.Constant.t
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
...
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
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