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 DPset : sig ... end
module DPmap : 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 type EqType = sig ... end
module type QNameS = 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
module Ind : sig ... end
type inductive = Ind.t
module Construct : sig ... end
type constructor = Construct.t
module Indset : sig ... end
module Constrset : sig ... end
module Indset_env : sig ... end
module Constrset_env : sig ... end
module Indmap : sig ... end
module Constrmap : sig ... end
module Indmap_env : sig ... end
module Constrmap_env : sig ... end
val ind_modpath : inductive -> ModPath.t
  • deprecated Use the Ind module
val constr_modpath : constructor -> ModPath.t
  • deprecated Use the Construct module
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
  • deprecated Use the Ind module
val eq_user_ind : inductive -> inductive -> bool
  • deprecated Use the Ind module
val eq_syntactic_ind : inductive -> inductive -> bool
  • deprecated Use the Ind module
val ind_ord : inductive -> inductive -> int
  • deprecated Use the Ind module
val ind_hash : inductive -> int
  • deprecated Use the Ind module
val ind_user_ord : inductive -> inductive -> int
  • deprecated Use the Ind module
val ind_user_hash : inductive -> int
  • deprecated Use the Ind module
val ind_syntactic_ord : inductive -> inductive -> int
  • deprecated Use the Ind module
val ind_syntactic_hash : inductive -> int
  • deprecated Use the Ind module
val eq_constructor : constructor -> constructor -> bool
  • deprecated Use the Construct module
val eq_user_constructor : constructor -> constructor -> bool
  • deprecated Use the Construct module
val eq_syntactic_constructor : constructor -> constructor -> bool
  • deprecated Use the Construct module
val constructor_ord : constructor -> constructor -> int
  • deprecated Use the Construct module
val constructor_hash : constructor -> int
  • deprecated Use the Construct module
val constructor_user_ord : constructor -> constructor -> int
  • deprecated Use the Construct module
val constructor_user_hash : constructor -> int
  • deprecated Use the Construct module
val constructor_syntactic_ord : constructor -> constructor -> int
  • deprecated Use the Construct module
val constructor_syntactic_hash : constructor -> int
  • deprecated Use the Construct module
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 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_ind_chk : inductive -> inductive -> bool
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
module Projection : sig ... end
module GlobRef : sig ... end
type evaluable_global_reference =
  1. | EvalVarRef of Id.t
  2. | EvalConstRef of Constant.t
type lident = Id.t CAst.t
type lname = Name.t CAst.t
type lstring = string CAst.t
val lident_eq : lident -> lident -> bool
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