diff options
| author | Guillaume Melquiond | 2020-12-27 14:55:17 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-01-10 10:24:10 +0100 |
| commit | 5820a964a5b380d82923be7905cdacd6fa6bd6c3 (patch) | |
| tree | 13854701b6ad63b08c49ebf29a9078f917829cdd /kernel/vmemitcodes.ml | |
| parent | d1215d47c3cda09f4df2f07ce9362b3e6fc5b164 (diff) | |
Remove MAKEPROD.
MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is
never encountered in the fast path, this optimization is not worth the
extra complexity.
Diffstat (limited to 'kernel/vmemitcodes.ml')
| -rw-r--r-- | kernel/vmemitcodes.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index 85b5ca03e5..d3af8bf09b 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -337,8 +337,6 @@ let emit_instr env = function if Int.equal n 0 then invalid_arg "emit_instr : block size = 0" else if n < 4 then (out env(opMAKEBLOCK1 + n - 1); out_int env t) else (out env opMAKEBLOCK; out_int env n; out_int env t) - | Kmakeprod -> - out env opMAKEPROD | Kmakeswitchblock(typlbl,swlbl,annot,sz) -> out env opMAKESWITCHBLOCK; out_label env typlbl; out_label env swlbl; |