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
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
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