diff options
| author |  Benjamin Gregoire <Benjamin.Gregoire@inria.fr> | 2015-03-26 19:00:00 +0100 |
|---|---|---|
| committer | Benjamin Gregoire <Benjamin.Gregoire@inria.fr> | 2015-03-26 19:00:00 +0100 |
| commit | 00894adf6fc11f4336a3ece0c347676bbf0b4c11 (patch) | |
| tree | a3d46465df90fac47629a483f6cd75be40d9656e /kernel/cemitcodes.ml | |
| parent | f920ae56ffacf80f85dcf33d3f1ccf0acb4375b1 (diff) | |
allows the vm to deal with inductive type with 8388607 constant constructors and 8388851 non-constant constructor.
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index c5f88f6f5..aa1bba02d 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -223,7 +223,7 @@ let emit_instr = function slot_for_annot annot;out_int sz | Kswitch (tbl_const, tbl_block) -> out opSWITCH; - out_int (Array.length tbl_const + (Array.length tbl_block lsl 16)); + out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); let org = !out_position in Array.iter (out_label_with_orig org) tbl_const; Array.iter (out_label_with_orig org) tbl_block |