aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytegen.ml
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/cbytegen.ml
parentd1da0509fe8c26a7e5c41b610866a7d00e635e77 (diff)
[VM] Move structured_constant to Vmvalues
Diffstat (limited to 'kernel/cbytegen.ml')
-rw-r--r--kernel/cbytegen.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index e336ea922d..4c9ffc891e 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -14,6 +14,7 @@
open Util
open Names
+open Vmvalues
open Cbytecodes
open Cemitcodes
open Cinstr