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
  • deprecated Use Name.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 global_reference =
  1. | VarRef of variable
  2. | ConstRef of Constant.t
  3. | IndRef of inductive
  4. | ConstructRef of constructor
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
  • deprecated Same as [Constant.UserOrd.equal].
val eq_ind_chk : inductive -> inductive -> bool
type identifier = Id.t
  • deprecated Alias for [Id.t]
val string_of_id : Id.t -> string
  • deprecated Same as [Id.to_string].
val id_of_string : string -> Id.t
  • deprecated Same as [Id.of_string].
val id_ord : Id.t -> Id.t -> int
  • deprecated Same as [Id.compare].
val id_eq : Id.t -> Id.t -> bool
  • deprecated Same as [Id.equal].
module Idset : sig ... end
module Idpred : sig ... end
module Idmap : sig ... end
type dir_path = DirPath.t
  • deprecated Alias for [DirPath.t].
val dir_path_ord : DirPath.t -> DirPath.t -> int
  • deprecated Same as [DirPath.compare].
val dir_path_eq : DirPath.t -> DirPath.t -> bool
  • deprecated Same as [DirPath.equal].
val make_dirpath : module_ident list -> DirPath.t
  • deprecated Same as [DirPath.make].
val repr_dirpath : DirPath.t -> module_ident list
  • deprecated Same as [DirPath.repr].
val empty_dirpath : DirPath.t
  • deprecated Same as [DirPath.empty].
val is_empty_dirpath : DirPath.t -> bool
  • deprecated Same as [DirPath.is_empty].
val string_of_dirpath : DirPath.t -> string
  • deprecated Same as [DirPath.to_string].
val initial_dir : DirPath.t
  • deprecated Same as [DirPath.initial].
type label = Label.t
  • deprecated Same as [Label.t].
val mk_label : string -> Label.t
  • deprecated Same as [Label.make].
val string_of_label : Label.t -> string
  • deprecated Same as [Label.to_string].
val pr_label : Label.t -> Pp.t
  • deprecated Same as [Label.print].
val label_of_id : Id.t -> Label.t
  • deprecated Same as [Label.of_id].
val id_of_label : Label.t -> Id.t
  • deprecated Same as [Label.to_id].
val eq_label : Label.t -> Label.t -> bool
  • deprecated Same as [Label.equal].
type mod_bound_id = MBId.t
  • deprecated Same as [MBId.t].
val mod_bound_id_ord : MBId.t -> MBId.t -> int
  • deprecated Same as [MBId.compare].
val mod_bound_id_eq : MBId.t -> MBId.t -> bool
  • deprecated Same as [MBId.equal].
val make_mbid : DirPath.t -> Id.t -> MBId.t
  • deprecated Same as [MBId.make].
val repr_mbid : MBId.t -> int * Id.t * DirPath.t
  • deprecated Same as [MBId.repr].
val id_of_mbid : MBId.t -> Id.t
  • deprecated Same as [MBId.to_id].
val string_of_mbid : MBId.t -> string
  • deprecated Same as [MBId.to_string].
val debug_string_of_mbid : MBId.t -> string
  • deprecated Same as [MBId.debug_to_string].
val name_eq : Name.t -> Name.t -> bool
  • deprecated Same as [Name.equal].
type module_path = ModPath.t =
  1. | MPfile of DirPath.t
  2. | MPbound of MBId.t
  3. | MPdot of ModPath.t * Label.t
  • deprecated Alias type
val mp_ord : ModPath.t -> ModPath.t -> int
  • deprecated Same as [ModPath.compare].
val mp_eq : ModPath.t -> ModPath.t -> bool
  • deprecated Same as [ModPath.equal].
val check_bound_mp : ModPath.t -> bool
  • deprecated Same as [ModPath.is_bound].
val string_of_mp : ModPath.t -> string
  • deprecated Same as [ModPath.to_string].
val initial_path : ModPath.t
  • deprecated Same as [ModPath.initial].
type kernel_name = KerName.t
  • deprecated Alias type
val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t
  • deprecated Same as [KerName.make].
val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t
  • deprecated Same as [KerName.repr].
val modpath : KerName.t -> ModPath.t
  • deprecated Same as [KerName.modpath].
val label : KerName.t -> Label.t
  • deprecated Same as [KerName.label].
val string_of_kn : KerName.t -> string
  • deprecated Same as [KerName.to_string].
val pr_kn : KerName.t -> Pp.t
  • deprecated Same as [KerName.print].
val kn_ord : KerName.t -> KerName.t -> int
  • deprecated Same as [KerName.compare].
type constant = Constant.t
  • deprecated Alias type
module Projection : sig ... end
type projection = Projection.t
  • deprecated Alias for [Projection.t]
val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t
  • deprecated Same as [Constant.make]
val constant_of_kn : KerName.t -> Constant.t
  • deprecated Same as [Constant.make1]
val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t
  • deprecated Same as [Constant.make3]
val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t
  • deprecated Same as [Constant.repr3]
val user_con : Constant.t -> KerName.t
  • deprecated Same as [Constant.user]
val canonical_con : Constant.t -> KerName.t
  • deprecated Same as [Constant.canonical]
val con_modpath : Constant.t -> ModPath.t
  • deprecated Same as [Constant.modpath]
val con_label : Constant.t -> Label.t
  • deprecated Same as [Constant.label]
val eq_constant : Constant.t -> Constant.t -> bool
  • deprecated Same as [Constant.equal]
val con_ord : Constant.t -> Constant.t -> int
  • deprecated Same as [Constant.CanOrd.compare]
val con_user_ord : Constant.t -> Constant.t -> int
  • deprecated Same as [Constant.UserOrd.compare]
val con_with_label : Constant.t -> Label.t -> Constant.t
  • deprecated Same as [Constant.change_label]
val string_of_con : Constant.t -> string
  • deprecated Same as [Constant.to_string]
val pr_con : Constant.t -> Pp.t
  • deprecated Same as [Constant.print]
val debug_pr_con : Constant.t -> Pp.t
  • deprecated Same as [Constant.debug_print]
val debug_string_of_con : Constant.t -> string
  • deprecated Same as [Constant.debug_to_string]
type mutual_inductive = MutInd.t
  • deprecated Alias type
val mind_of_kn : KerName.t -> MutInd.t
  • deprecated Same as [MutInd.make1]
val mind_of_kn_equiv : KerName.t -> KerName.t -> MutInd.t
  • deprecated Same as [MutInd.make]
val make_mind : ModPath.t -> DirPath.t -> Label.t -> MutInd.t
  • deprecated Same as [MutInd.make3]
val user_mind : MutInd.t -> KerName.t
  • deprecated Same as [MutInd.user]
val canonical_mind : MutInd.t -> KerName.t
  • deprecated Same as [MutInd.canonical]
val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t
  • deprecated Same as [MutInd.repr3]
val eq_mind : MutInd.t -> MutInd.t -> bool
  • deprecated Same as [MutInd.equal]
val mind_ord : MutInd.t -> MutInd.t -> int
  • deprecated Same as [MutInd.CanOrd.compare]
val mind_user_ord : MutInd.t -> MutInd.t -> int
  • deprecated Same as [MutInd.UserOrd.compare]
val mind_label : MutInd.t -> Label.t
  • deprecated Same as [MutInd.label]
val mind_modpath : MutInd.t -> ModPath.t
  • deprecated Same as [MutInd.modpath]
val string_of_mind : MutInd.t -> string
  • deprecated Same as [MutInd.to_string]
val pr_mind : MutInd.t -> Pp.t
  • deprecated Same as [MutInd.print]
val debug_pr_mind : MutInd.t -> Pp.t
  • deprecated Same as [MutInd.debug_print]
val debug_string_of_mind : MutInd.t -> string
  • deprecated Same as [MutInd.debug_to_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