package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type message = string
val find_reference : message -> string list -> string -> Globnames.global_reference
val coq_reference : message -> string list -> string -> Globnames.global_reference
val check_required_library : string list -> unit
val gen_reference_in_modules : string -> string list list -> string -> Globnames.global_reference
val arith_modules : string list list
val zarith_base_modules : string list list
val init_modules : string list list
val prelude_module : Names.DirPath.t
val logic_module : Names.DirPath.t
val logic_module_name : string list
val logic_type_module : Names.DirPath.t
val jmeq_module : Names.DirPath.t
val jmeq_module_name : string list
val datatypes_module_name : string list
val type_of_id : Names.constant
val nat_path : Libnames.full_path
val path_of_O : Names.constructor
val path_of_S : Names.constructor
val path_of_true : Names.constructor
val path_of_false : Names.constructor
val glob_identity : Globnames.global_reference
type coq_bool_data = {
  1. andb : Globnames.global_reference;
  2. andb_prop : Globnames.global_reference;
  3. andb_true_intro : Globnames.global_reference;
}
val build_bool_type : coq_bool_data Util.delayed
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
val build_prod : coq_sigma_data Util.delayed
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 build_coq_f_equal2 : Globnames.global_reference Util.delayed
type coq_inversion_data = {
  1. inv_eq : Globnames.global_reference;
  2. inv_ind : Globnames.global_reference;
  3. inv_congr : Globnames.global_reference;
}
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_iff_left_proj : Globnames.global_reference Util.delayed
val build_coq_iff_right_proj : Globnames.global_reference Util.delayed
val coq_eq_ref : Globnames.global_reference lazy_t
val coq_identity_ref : Globnames.global_reference lazy_t
val coq_jmeq_ref : Globnames.global_reference lazy_t
val coq_eq_true_ref : Globnames.global_reference lazy_t
val coq_existS_ref : Globnames.global_reference lazy_t
val coq_existT_ref : Globnames.global_reference lazy_t
val coq_exist_ref : Globnames.global_reference lazy_t
val coq_not_ref : Globnames.global_reference lazy_t
val coq_False_ref : Globnames.global_reference lazy_t
val coq_sumbool_ref : Globnames.global_reference lazy_t
val coq_sig_ref : Globnames.global_reference lazy_t
val coq_or_ref : Globnames.global_reference lazy_t
val coq_iff_ref : Globnames.global_reference lazy_t
val gen_reference : message -> string list -> string -> Globnames.global_reference
  • deprecated Please use Coqlib.find_reference
OCaml

Innovation. Community. Security.