aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmemitcodes.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-10-21 08:56:36 +0000
committerGitHub2020-10-21 08:56:36 +0000
commit637657847c6215e031947de042b927a9efd34edd (patch)
tree421b6b984b6d3aec4bc77e9e97dd6d7a6d2b2038 /kernel/vmemitcodes.ml
parent91e7863e64a5741b6530828c1642d765ddff41ae (diff)
parentc3cfb3c26241c374545380f08aa4345eb553000e (diff)
Merge PR #12955: Reroot primitive arrays on access
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/vmemitcodes.ml')
-rw-r--r--kernel/vmemitcodes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index f913cb906c..ec8601edc9 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -262,7 +262,7 @@ let check_prim_op = function
| Arraymake -> opISINT_CAML_CALL2
| Arrayget -> opISARRAY_INT_CAML_CALL2
| Arrayset -> opISARRAY_INT_CAML_CALL3
- | Arraydefault | Arraycopy | Arrayreroot | Arraylength ->
+ | Arraydefault | Arraycopy | Arraylength ->
opISARRAY_CAML_CALL1
let emit_instr env = function