package coq
val accu_tag : tagval type_atom_tag : tagval max_atom_tag : tagval proj_tag : tagval fix_app_tag : tagval switch_tag : tagval cofix_tag : tagval cofix_evaluated_tag : tagval last_variant_tag : tagtype structured_constant = | Const_sort of Sorts.t| Const_ind of Names.inductive| Const_proj of Names.Constant.t| Const_b0 of tag| Const_bn of tag * structured_constant array| Const_univ_level of Univ.Level.t
val pp_struct_const : structured_constant -> Pp.ttype reloc_table = (tag * int) arraytype annot_switch = {ci : Constr.case_info;rtbl : reloc_table;tailcall : bool;max_stack_size : int;
}val eq_structured_constant : structured_constant -> structured_constant -> boolval hash_structured_constant : structured_constant -> intval eq_annot_switch : annot_switch -> annot_switch -> boolval hash_annot_switch : annot_switch -> intmodule Label : sig ... endtype instruction = | Klabel of Label.t| Kacc of int| Kenvacc of int| Koffsetclosure of int| Kpush| Kpop of int| Kpush_retaddr of Label.t| Kapply of int| Kappterm of int * int| Kreturn of int| Kjump| Krestart| Kgrab of int| Kgrabrec of int| Kclosure of Label.t * int| Kclosurerec of int * int * Label.t array * Label.t array| Kclosurecofix of int * int * Label.t array * Label.t array| Kgetglobal of Names.Constant.t| Kconst of structured_constant| Kmakeblock of int * tag| Kmakeprod| Kmakeswitchblock of Label.t * Label.t * annot_switch * int| Kswitch of Label.t array * Label.t array| Kpushfields of int| Kfield of int| Ksetfield of int| Kstop| Ksequence of bytecodes * bytecodes| Kproj of int * Names.Constant.t| Kensurestackcapacity of int| Kbranch of Label.t| Kaddint31| Kaddcint31| Kaddcarrycint31| Ksubint31| Ksubcint31| Ksubcarrycint31| Kmulint31| Kmulcint31| Kdiv21int31| Kdivint31| Kaddmuldivint31| Kcompareint31| Khead0int31| Ktail0int31| Kisconst of Label.t| Kareconst of int * Label.t| Kcompint31| Kdecompint31| Klorint31| Klandint31| Klxorint31
and bytecodes = instruction listtype fv = fv_elem arraymodule FvMap : sig ... endtype comp_env = {arity : int;nb_uni_stack : int;nb_stack : int;in_stack : int list;nb_rec : int;pos_rec : instruction list;offset : int;in_env : vm_env ref;
}