package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Id : sig ... end
module Name : sig ... end
type name = Name.t =
  1. | Anonymous
  2. | Name of Id.t
type variable = Id.t
type module_ident = Id.t
module ModIdset : sig ... end
module ModIdmap : sig ... end
module DirPath : sig ... end
module Label : sig ... end
module MBId : sig ... end
module MBIset : sig ... end
module MBImap : sig ... end
module ModPath : sig ... end
module MPset : sig ... end
module MPmap : sig ... end
module KerName : sig ... end
module KNset : sig ... end
module KNpred : sig ... end
module KNmap : sig ... end
module Constant : sig ... end
module Cpred : sig ... end
module Cset : sig ... end
module Cset_env : sig ... end
module Cmap : sig ... end
module Cmap_env : sig ... end
module MutInd : sig ... end
module Mindset : sig ... end
module Mindmap : sig ... end
module Mindmap_env : sig ... end
type inductive = MutInd.t * int
type constructor = inductive * int
module Indmap : sig ... end
module Constrmap : sig ... end
module Indmap_env : sig ... end
module Constrmap_env : sig ... end
val ind_modpath : inductive -> ModPath.t
val constr_modpath : constructor -> ModPath.t
val ith_mutual_inductive : inductive -> int -> inductive
val ith_constructor_of_inductive : inductive -> int -> constructor
val inductive_of_constructor : constructor -> inductive
val index_of_constructor : constructor -> int
val eq_ind : inductive -> inductive -> bool
val eq_user_ind : inductive -> inductive -> bool
val eq_syntactic_ind : inductive -> inductive -> bool
val ind_ord : inductive -> inductive -> int
val ind_hash : inductive -> int
val ind_user_ord : inductive -> inductive -> int
val ind_user_hash : inductive -> int
val ind_syntactic_ord : inductive -> inductive -> int
val ind_syntactic_hash : inductive -> int
val eq_constructor : constructor -> constructor -> bool
val eq_user_constructor : constructor -> constructor -> bool
val eq_syntactic_constructor : constructor -> constructor -> bool
val constructor_ord : constructor -> constructor -> int
val constructor_hash : constructor -> int
val constructor_user_ord : constructor -> constructor -> int
val constructor_user_hash : constructor -> int
val constructor_syntactic_ord : constructor -> constructor -> int
val constructor_syntactic_hash : constructor -> int
type evaluable_global_reference =
  1. | EvalVarRef of Id.t
  2. | EvalConstRef of Constant.t
val hcons_con : Constant.t -> Constant.t
val hcons_mind : MutInd.t -> MutInd.t
val hcons_ind : inductive -> inductive
val hcons_construct : constructor -> constructor
type !'a tableKey =
  1. | ConstKey of 'a
  2. | VarKey of Id.t
  3. | RelKey of Int.t
type transparent_state = Id.Pred.t * Cpred.t
val empty_transparent_state : transparent_state
val full_transparent_state : transparent_state
val var_full_transparent_state : transparent_state
val cst_full_transparent_state : transparent_state
type inv_rel_key = int
val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool
val eq_constant_key : Constant.t -> Constant.t -> bool
val eq_con_chk : Constant.t -> Constant.t -> bool
val eq_ind_chk : inductive -> inductive -> bool
type identifier = Id.t
val string_of_id : identifier -> string
val id_of_string : string -> identifier
val id_ord : identifier -> identifier -> int
val id_eq : identifier -> identifier -> bool
module Idset : sig ... end
module Idpred : sig ... end
module Idmap : sig ... end
type dir_path = DirPath.t
val dir_path_ord : dir_path -> dir_path -> int
val dir_path_eq : dir_path -> dir_path -> bool
val make_dirpath : module_ident list -> dir_path
val repr_dirpath : dir_path -> module_ident list
val empty_dirpath : dir_path
val is_empty_dirpath : dir_path -> bool
val string_of_dirpath : dir_path -> string
val initial_dir : DirPath.t
type label = Label.t
val mk_label : string -> label
val string_of_label : label -> string
val pr_label : label -> Pp.std_ppcmds
val label_of_id : Id.t -> label
val id_of_label : label -> Id.t
val eq_label : label -> label -> bool
type mod_bound_id = MBId.t
val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
val make_mbid : DirPath.t -> Id.t -> mod_bound_id
val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t
val id_of_mbid : mod_bound_id -> Id.t
val string_of_mbid : mod_bound_id -> string
val debug_string_of_mbid : mod_bound_id -> string
val name_eq : name -> name -> bool
type module_path = ModPath.t =
  1. | MPfile of DirPath.t
  2. | MPbound of MBId.t
  3. | MPdot of module_path * Label.t
val mp_ord : module_path -> module_path -> int
val mp_eq : module_path -> module_path -> bool
val check_bound_mp : module_path -> bool
val string_of_mp : module_path -> string
val initial_path : module_path
type kernel_name = KerName.t
val make_kn : ModPath.t -> DirPath.t -> Label.t -> kernel_name
val modpath : kernel_name -> module_path
val label : kernel_name -> Label.t
val string_of_kn : kernel_name -> string
val pr_kn : kernel_name -> Pp.std_ppcmds
val kn_ord : kernel_name -> kernel_name -> int
type constant = Constant.t
module Projection : sig ... end
type projection = Projection.t
val constant_of_kn_equiv : KerName.t -> KerName.t -> constant
val constant_of_kn : KerName.t -> constant
val make_con : ModPath.t -> DirPath.t -> Label.t -> constant
val repr_con : constant -> ModPath.t * DirPath.t * Label.t
val user_con : constant -> KerName.t
val canonical_con : constant -> KerName.t
val con_modpath : constant -> ModPath.t
val con_label : constant -> Label.t
val eq_constant : constant -> constant -> bool
val con_ord : constant -> constant -> int
val con_user_ord : constant -> constant -> int
val con_with_label : constant -> Label.t -> constant
val string_of_con : constant -> string
val pr_con : constant -> Pp.std_ppcmds
val debug_pr_con : constant -> Pp.std_ppcmds
val debug_string_of_con : constant -> string
type mutual_inductive = MutInd.t
val mind_of_kn : KerName.t -> mutual_inductive
val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive
val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive
val user_mind : mutual_inductive -> KerName.t
val canonical_mind : mutual_inductive -> KerName.t
val eq_mind : mutual_inductive -> mutual_inductive -> bool
val mind_ord : mutual_inductive -> mutual_inductive -> int
val mind_user_ord : mutual_inductive -> mutual_inductive -> int
val mind_label : mutual_inductive -> Label.t
val mind_modpath : mutual_inductive -> ModPath.t
val string_of_mind : mutual_inductive -> string
val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds
val debug_string_of_mind : mutual_inductive -> string
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct