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