package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val register_ref : string -> Names.GlobRef.t -> unit
val lib_ref : string -> Names.GlobRef.t
val has_ref : string -> bool
val check_ind_ref : string -> Names.inductive -> bool
val get_lib_refs : unit -> (string * Names.GlobRef.t) list
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
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 check_required_library : string list -> unit
val datatypes_module_name : string list
val logic_module_name : string list
val jmeq_module_name : string list
val find_reference : string -> string list -> string -> Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val coq_reference : string -> string list -> string -> Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val gen_reference_in_modules : string -> string list list -> string -> Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val arith_modules : string list list
  • deprecated Please use Coqlib.lib_ref
val zarith_base_modules : string list list
  • deprecated Please use Coqlib.lib_ref
val init_modules : string list list
  • deprecated Please use Coqlib.lib_ref
val logic_module : Names.ModPath.t
  • deprecated Please use Coqlib.lib_ref
val logic_type_module : Names.DirPath.t
  • deprecated Please use Coqlib.lib_ref
  • deprecated Please use Coqlib.lib_ref
val type_of_id : Names.Constant.t
  • deprecated Please use Coqlib.lib_ref
val nat_path : Libnames.full_path
  • deprecated Please use Coqlib.lib_ref
val glob_nat : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val path_of_O : Names.constructor
  • deprecated Please use Coqlib.lib_ref
val path_of_S : Names.constructor
  • deprecated Please use Coqlib.lib_ref
val glob_O : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val glob_S : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val glob_bool : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val path_of_true : Names.constructor
  • deprecated Please use Coqlib.lib_ref
val path_of_false : Names.constructor
  • deprecated Please use Coqlib.lib_ref
val glob_true : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val glob_false : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val glob_eq : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val glob_identity : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
val glob_jmeq : Names.GlobRef.t
  • deprecated Please use Coqlib.lib_ref
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
  • deprecated Please use Coqlib.lib_ref
val build_prod : coq_sigma_data Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_eq : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_eq_refl : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_eq_sym : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_f_equal2 : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
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
  • deprecated Please use Coqlib.lib_ref
val build_coq_inversion_identity_data : coq_inversion_data Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_inversion_jmeq_data : coq_inversion_data Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_inversion_eq_true_data : coq_inversion_data Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_sumbool : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_False : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_True : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_I : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_not : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_and : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_conj : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_iff : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_iff_left_proj : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_iff_right_proj : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_prod : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_pair : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_or : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val build_coq_ex : Names.GlobRef.t Util.delayed
  • deprecated Please use Coqlib.lib_ref
val coq_eq_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_identity_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_jmeq_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_eq_true_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_existS_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_existT_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_exist_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_not_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_False_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_sumbool_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_sig_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_or_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref
val coq_iff_ref : Names.GlobRef.t lazy_t
  • deprecated Please use Coqlib.lib_ref