coq 8.12.2 · OCaml Package

coq

type t = t -> t

type accumulator

type tag = int

type arity = int

type reloc_table = (tag * arity) array

type annot_sw = {

asw_ind : Names.inductive;
asw_ci : Constr.case_info;
asw_reloc : reloc_table;
asw_finite : bool;
asw_prefix : string;

}

val eq_annot_sw : annot_sw -> annot_sw -> bool

val hash_annot_sw : annot_sw -> int

type sort_annot = string * int

type rec_pos = int array

val eq_rec_pos : rec_pos -> rec_pos -> bool

type atom =

| Arel of int
| Aconstant of Constr.pconstant
| Aind of Constr.pinductive
| Asort of Sorts.t
| Avar of Names.Id.t
| Acase of annot_sw * accumulator * t * t -> t
| Afix of t array * t array * rec_pos * int
| Acofix of t array * t array * int * t
| Acofixe of t array * t array * int * t
| Aprod of Names.Name.t * t * t -> t
| Ameta of Constr.metavariable * t
| Aevar of Evar.t * t array
| Aproj of Names.inductive * int * accumulator

type symbol =

| SymbValue of t
| SymbSort of Sorts.t
| SymbName of Names.Name.t
| SymbConst of Names.Constant.t
| SymbMatch of annot_sw
| SymbInd of Names.inductive
| SymbMeta of Constr.metavariable
| SymbEvar of Evar.t
| SymbLevel of Univ.Level.t
| SymbProj of Names.inductive * int

type symbols = symbol array

val empty_symbols : symbols

val mk_accu : atom -> t

val mk_rel_accu : int -> t

val mk_rels_accu : int -> int -> t array

val mk_constant_accu : Names.Constant.t -> Univ.Level.t array -> t

val mk_ind_accu : Names.inductive -> Univ.Level.t array -> t

val mk_sort_accu : Sorts.t -> Univ.Level.t array -> t

val mk_var_accu : Names.Id.t -> t

val mk_sw_accu : annot_sw -> accumulator -> t -> t -> t

val mk_prod_accu : Names.Name.t -> t -> t -> t

val mk_fix_accu : rec_pos -> int -> t array -> t array -> t

val mk_cofix_accu : int -> t array -> t array -> t

val mk_meta_accu : Constr.metavariable -> t

val mk_evar_accu : Evar.t -> t array -> t

val mk_proj_accu : (Names.inductive * int) -> accumulator -> t

val upd_cofix : t -> t -> unit

val force_cofix : t -> t

val mk_const : tag -> t

val mk_block : tag -> t array -> t

val mk_bool : bool -> t

val mk_int : int -> t

val mk_uint : Uint63.t -> t

val mk_float : Float64.t -> t

val napply : t -> t array -> t

val dummy_value : unit -> t

val atom_of_accu : accumulator -> atom

val args_of_accu : accumulator -> t array

val accu_nargs : accumulator -> int

val cast_accu : t -> accumulator

type block

val block_size : block -> int

val block_field : block -> int -> t

val block_tag : block -> int

type kind_of_value =

| Vaccu of accumulator
| Vfun of t -> t
| Vconst of int
| Vint64 of int64
| Vfloat64 of float
| Vblock of block

val kind_of_value : t -> kind_of_value

val str_encode : 'a -> string

val str_decode : string -> 'a

val val_to_int : t -> int

val is_int : t -> bool

val head0 : t -> t -> t

val tail0 : t -> t -> t

val add : t -> t -> t -> t

val sub : t -> t -> t -> t

val mul : t -> t -> t -> t

val div : t -> t -> t -> t

val rem : t -> t -> t -> t

val l_sr : t -> t -> t -> t

val l_sl : t -> t -> t -> t

val l_and : t -> t -> t -> t

val l_xor : t -> t -> t -> t

val l_or : t -> t -> t -> t

val addc : t -> t -> t -> t

val subc : t -> t -> t -> t

val addCarryC : t -> t -> t -> t

val subCarryC : t -> t -> t -> t

val mulc : t -> t -> t -> t

val diveucl : t -> t -> t -> t

val div21 : t -> t -> t -> t -> t

val addMulDiv : t -> t -> t -> t -> t

val eq : t -> t -> t -> t

val lt : t -> t -> t -> t

val le : t -> t -> t -> t

val compare : t -> t -> t -> t

val print : t -> t

val no_check_head0 : t -> t

val no_check_tail0 : t -> t

val no_check_add : t -> t -> t

val no_check_sub : t -> t -> t

val no_check_mul : t -> t -> t

val no_check_div : t -> t -> t

val no_check_rem : t -> t -> t

val no_check_l_sr : t -> t -> t

val no_check_l_sl : t -> t -> t

val no_check_l_and : t -> t -> t

val no_check_l_xor : t -> t -> t

val no_check_l_or : t -> t -> t

val no_check_addc : t -> t -> t

val no_check_subc : t -> t -> t

val no_check_addCarryC : t -> t -> t

val no_check_subCarryC : t -> t -> t

val no_check_mulc : t -> t -> t

val no_check_diveucl : t -> t -> t

val no_check_div21 : t -> t -> t -> t

val no_check_addMulDiv : t -> t -> t -> t

val no_check_eq : t -> t -> t

val no_check_lt : t -> t -> t

val no_check_le : t -> t -> t

val no_check_compare : t -> t -> t

val is_float : t -> bool

val fopp : t -> t -> t

val fabs : t -> t -> t

val feq : t -> t -> t -> t

val flt : t -> t -> t -> t

val fle : t -> t -> t -> t

val fcompare : t -> t -> t -> t

val fclassify : t -> t -> t

val fadd : t -> t -> t -> t

val fsub : t -> t -> t -> t

val fmul : t -> t -> t -> t

val fdiv : t -> t -> t -> t

val fsqrt : t -> t -> t

val float_of_int : t -> t -> t

val normfr_mantissa : t -> t -> t

val frshiftexp : t -> t -> t

val ldshiftexp : t -> t -> t -> t

val next_up : t -> t -> t

val next_down : t -> t -> t

val no_check_fopp : t -> t

val no_check_fabs : t -> t

val no_check_feq : t -> t -> t

val no_check_flt : t -> t -> t

val no_check_fle : t -> t -> t

val no_check_fcompare : t -> t -> t

val no_check_fclassify : t -> t

val no_check_fadd : t -> t -> t

val no_check_fsub : t -> t -> t

val no_check_fmul : t -> t -> t

val no_check_fdiv : t -> t -> t

val no_check_fsqrt : t -> t

val no_check_float_of_int : t -> t

val no_check_normfr_mantissa : t -> t

val no_check_frshiftexp : t -> t

val no_check_ldshiftexp : t -> t -> t

val no_check_next_up : t -> t

val no_check_next_down : t -> t

package coq