coq 8.7.1 · OCaml Package

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 id : Names.constant

val type_of_id : Names.constant

val nat_path : Libnames.full_path

val glob_nat : Globnames.global_reference

val path_of_O : Names.constructor

val path_of_S : Names.constructor

val glob_O : Globnames.global_reference

val glob_S : Globnames.global_reference

val glob_bool : Globnames.global_reference

val path_of_true : Names.constructor

val path_of_false : Names.constructor

val glob_true : Globnames.global_reference

val glob_false : Globnames.global_reference

val glob_eq : Globnames.global_reference

val glob_identity : Globnames.global_reference

val glob_jmeq : Globnames.global_reference

type coq_bool_data = {

andb : Globnames.global_reference;
andb_prop : Globnames.global_reference;
andb_true_intro : Globnames.global_reference;

}

val build_bool_type : coq_bool_data Util.delayed

type coq_sigma_data = {

}

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

type coq_eq_data = {

}

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_eq : Globnames.global_reference Util.delayed

val build_coq_eq_refl : Globnames.global_reference Util.delayed

val build_coq_eq_sym : Globnames.global_reference Util.delayed

val build_coq_f_equal2 : Globnames.global_reference Util.delayed

type coq_inversion_data = {

inv_eq : Globnames.global_reference;
inv_ind : Globnames.global_reference;
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_sumbool : Globnames.global_reference Util.delayed

val build_coq_False : Globnames.global_reference Util.delayed

val build_coq_True : Globnames.global_reference Util.delayed

val build_coq_I : Globnames.global_reference Util.delayed

val build_coq_not : Globnames.global_reference Util.delayed

val build_coq_and : Globnames.global_reference Util.delayed

val build_coq_conj : Globnames.global_reference Util.delayed

val build_coq_iff : Globnames.global_reference 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 build_coq_or : Globnames.global_reference Util.delayed

val build_coq_ex : 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

package coq