aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.mli
diff options
context:
space:
mode:
authorMaxime Dénès2018-03-01 14:43:07 +0100
committerMaxime Dénès2018-09-17 09:33:27 +0200
commitf02e6260f1cf1f49121860cfd95b6adb97db48ee (patch)
tree68e18977a37c01f4353f51cb2f4986c3d5ceeed5 /kernel/cemitcodes.mli
parentd1da0509fe8c26a7e5c41b610866a7d00e635e77 (diff)
[VM] Move structured_constant to Vmvalues
Diffstat (limited to 'kernel/cemitcodes.mli')
-rw-r--r--kernel/cemitcodes.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 9009926bdb..39ddf4a047 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -1,4 +1,5 @@
open Names
+open Vmvalues
open Cbytecodes
type reloc_info =