package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type message = string
val find_reference : message -> string list -> string -> Names.GlobRef.t
val coq_reference : message -> string list -> string -> Names.GlobRef.t
val check_required_library : string list -> unit
val gen_reference_in_modules : string -> string list list -> string -> Names.GlobRef.t
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.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
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
val glob_identity : Names.GlobRef.t
val glob_jmeq : Names.GlobRef.t
type coq_bool_data = {
  1. andb : Names.GlobRef.t;
  2. andb_prop : Names.GlobRef.t;
  3. andb_true_intro : Names.GlobRef.t;
}
val build_bool_type : coq_bool_data Util.delayed
type 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;
}
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 = {
  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;
}
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 : Names.GlobRef.t Util.delayed
val build_coq_eq_refl : Names.GlobRef.t Util.delayed
val build_coq_eq_sym : Names.GlobRef.t Util.delayed
val build_coq_f_equal2 : Names.GlobRef.t Util.delayed
type coq_inversion_data = {
  1. inv_eq : Names.GlobRef.t;
  2. inv_ind : Names.GlobRef.t;
  3. inv_congr : Names.GlobRef.t;
}
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
val build_coq_False : Names.GlobRef.t Util.delayed
val build_coq_True : Names.GlobRef.t Util.delayed
val build_coq_I : Names.GlobRef.t Util.delayed
val build_coq_not : Names.GlobRef.t Util.delayed
val build_coq_and : Names.GlobRef.t Util.delayed
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_or : Names.GlobRef.t Util.delayed
val build_coq_ex : Names.GlobRef.t Util.delayed
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