aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytegen.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-03-02 21:46:55 +0100
committerMaxime Dénès2018-09-17 09:33:30 +0200
commit00a63b73f267ae90cc868f14ab4f36db8185b3e0 (patch)
treedb3c51106bf23f2cbb5a21109940f9b1623607ea /kernel/cbytegen.ml
parentf02e6260f1cf1f49121860cfd95b6adb97db48ee (diff)
[VM] Inject structured constants in values without reallocating them.
Diffstat (limited to 'kernel/cbytegen.ml')
-rw-r--r--kernel/cbytegen.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 4c9ffc891e..6dabfee4ef 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -491,7 +491,9 @@ let rec compile_lam env cenv lam sz cont =
match lam with
| Lrel(_, i) -> pos_rel i cenv sz :: cont
- | Lval v -> compile_structured_constant cenv v sz cont
+ | Lint i -> compile_structured_constant cenv (Const_b0 i) sz cont
+
+ | Lval v -> compile_structured_constant cenv (Const_val v) sz cont
| Lproj (p,arg) ->
compile_lam env cenv arg sz (Kproj p :: cont)