aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmbytecodes.mli
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-08-30 09:12:17 +0200
committerGuillaume Melquiond2020-11-13 15:13:23 +0100
commitaebc10aab3581a0561f96de6b5db6d530a65e658 (patch)
treefc77c92a0e39e4f77c4600ea4dc9e51f20a247b6 /kernel/vmbytecodes.mli
parentfdd16113a042170022dce276e53e7a3308c0451c (diff)
Remove some unused opcodes from VM.
Diffstat (limited to 'kernel/vmbytecodes.mli')
-rw-r--r--kernel/vmbytecodes.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli
index 33071b917b..138778eac4 100644
--- a/kernel/vmbytecodes.mli
+++ b/kernel/vmbytecodes.mli
@@ -61,7 +61,6 @@ type instruction =
| Kbranch of Label.t (** jump to label, is it needed ? *)
| Kprim of CPrimitives.t * pconstant
| Kcamlprim of CPrimitives.t * Label.t
- | Kareint of int
and bytecodes = instruction list