coq 8.7.2 · OCaml Package

module Id : sig ... end

module Name : sig ... end

type name = Name.t =

| Anonymous
| Name of Id.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 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

val eq_ind_chk : inductive -> inductive -> bool

type identifier = Id.t

val string_of_id : identifier -> string

val id_of_string : string -> identifier

val id_ord : identifier -> identifier -> int

val id_eq : identifier -> identifier -> bool

module Idset : sig ... end

module Idpred : sig ... end

module Idmap : sig ... end

type dir_path = DirPath.t

val dir_path_ord : dir_path -> dir_path -> int

val dir_path_eq : dir_path -> dir_path -> bool

val make_dirpath : module_ident list -> dir_path

val repr_dirpath : dir_path -> module_ident list

val empty_dirpath : dir_path

val is_empty_dirpath : dir_path -> bool

val string_of_dirpath : dir_path -> string

val initial_dir : DirPath.t

type label = Label.t

val mk_label : string -> label

val string_of_label : label -> string

val pr_label : label -> Pp.std_ppcmds

val label_of_id : Id.t -> label

val id_of_label : label -> Id.t

val eq_label : label -> label -> bool

type mod_bound_id = MBId.t

val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int

val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool

val make_mbid : DirPath.t -> Id.t -> mod_bound_id

val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t

val id_of_mbid : mod_bound_id -> Id.t

val string_of_mbid : mod_bound_id -> string

val debug_string_of_mbid : mod_bound_id -> string

val name_eq : name -> name -> bool

type module_path = ModPath.t =

| MPfile of DirPath.t
| MPbound of MBId.t
| MPdot of module_path * Label.t

val mp_ord : module_path -> module_path -> int

val mp_eq : module_path -> module_path -> bool

val check_bound_mp : module_path -> bool

val string_of_mp : module_path -> string

val initial_path : module_path

type kernel_name = KerName.t

val make_kn : ModPath.t -> DirPath.t -> Label.t -> kernel_name

val repr_kn : kernel_name -> module_path * DirPath.t * Label.t

val modpath : kernel_name -> module_path

val label : kernel_name -> Label.t

val string_of_kn : kernel_name -> string

val pr_kn : kernel_name -> Pp.std_ppcmds

val kn_ord : kernel_name -> kernel_name -> int

type constant = Constant.t

module Projection : sig ... end

type projection = Projection.t

val constant_of_kn_equiv : KerName.t -> KerName.t -> constant

val constant_of_kn : KerName.t -> constant

val make_con : ModPath.t -> DirPath.t -> Label.t -> constant

val repr_con : constant -> ModPath.t * DirPath.t * Label.t

val user_con : constant -> KerName.t

val canonical_con : constant -> KerName.t

val con_modpath : constant -> ModPath.t

val con_label : constant -> Label.t

val eq_constant : constant -> constant -> bool

val con_ord : constant -> constant -> int

val con_user_ord : constant -> constant -> int

val con_with_label : constant -> Label.t -> constant

val string_of_con : constant -> string

val pr_con : constant -> Pp.std_ppcmds

val debug_pr_con : constant -> Pp.std_ppcmds

val debug_string_of_con : constant -> string

type mutual_inductive = MutInd.t

val mind_of_kn : KerName.t -> mutual_inductive

val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive

val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive

val user_mind : mutual_inductive -> KerName.t

val canonical_mind : mutual_inductive -> KerName.t

val repr_mind : mutual_inductive -> ModPath.t * DirPath.t * Label.t

val eq_mind : mutual_inductive -> mutual_inductive -> bool

val mind_ord : mutual_inductive -> mutual_inductive -> int

val mind_user_ord : mutual_inductive -> mutual_inductive -> int

val mind_label : mutual_inductive -> Label.t

val mind_modpath : mutual_inductive -> ModPath.t

val string_of_mind : mutual_inductive -> string

val pr_mind : mutual_inductive -> Pp.std_ppcmds

val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds

val debug_string_of_mind : mutual_inductive -> string

package coq