diff options
| author | Pierre-Marie Pédrot | 2018-09-17 16:49:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-17 16:49:45 +0200 |
| commit | f1482433ff225831d9937753f946cff2577b9309 (patch) | |
| tree | e59614016106e1672241f93cad4389d973093aa4 /kernel/cbytecodes.mli | |
| parent | eb2c11bf1c367d83cc45f4679d3bf15f25142d5c (diff) | |
| parent | a8bf1cab3f21de4a350737ef5c933af1746f54a1 (diff) | |
Merge PR #6906: [VM] Optimize structured values
Diffstat (limited to 'kernel/cbytecodes.mli')
| -rw-r--r-- | kernel/cbytecodes.mli | 36 |
1 files changed, 1 insertions, 35 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index f17a1e657e..9c04c166a2 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -11,41 +11,7 @@ (* $Id$ *) open Names -open Constr - -type tag = int - -val accu_tag : tag - -val type_atom_tag : tag -val max_atom_tag : tag -val proj_tag : tag -val fix_app_tag : tag -val switch_tag : tag -val cofix_tag : tag -val cofix_evaluated_tag : tag - -val last_variant_tag : tag - -type structured_constant = - | Const_sort of Sorts.t - | Const_ind of inductive - | 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.t - -type reloc_table = (tag * int) array - -type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} - -val eq_structured_constant : structured_constant -> structured_constant -> bool -val hash_structured_constant : structured_constant -> int - -val eq_annot_switch : annot_switch -> annot_switch -> bool -val hash_annot_switch : annot_switch -> int +open Vmvalues module Label : sig |