coq 8.8.1 · OCaml Package

module Id : sig ... end

module Name : sig ... end

type name = Name.t =

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

| VarRef of variable
| ConstRef of Constant.t
| IndRef of inductive
| ConstructRef of constructor

type evaluable_global_reference =

| EvalVarRef of Id.t
| EvalConstRef of Constant.t

val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool

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 =

| ConstKey of 'a
| VarKey of Id.t
| 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 =

| MPfile of DirPath.t
| MPbound of MBId.t
| 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]

package coq