aboutsummaryrefslogtreecommitdiff
path: root/pretyping
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 /pretyping
parentd1da0509fe8c26a7e5c41b610866a7d00e635e77 (diff)
[VM] Move structured_constant to Vmvalues
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/vnorm.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 255707dc7b..59e60aa8f4 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -161,9 +161,9 @@ and nf_whd env sigma whd typ =
| Vconstr_block b ->
let tag = btag b in
let (tag,ofs) =
- if tag = Cbytecodes.last_variant_tag then
+ if tag = last_variant_tag then
match whd_val (bfield b 0) with
- | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1)
+ | Vconstr_const tag -> (tag+last_variant_tag, 1)
| _ -> assert false
else (tag, 0) in
let capp,ctyp = construct_of_constr_block env tag typ in
@@ -278,7 +278,7 @@ and nf_stk ?from:(from=0) env sigma c t stk =
in
let branchs = Array.mapi mkbranch bsw in
let tcase = build_case_type p realargs c in
- let ci = sw.sw_annot.Cbytecodes.ci in
+ let ci = sw.sw_annot.Vmvalues.ci in
nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk
| Zproj p :: stk ->
assert (from = 0) ;