aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-07-06 16:18:33 +0200
committerPierre-Marie Pédrot2020-07-06 16:18:33 +0200
commit8907a5b7d2b91bff0b573956a05e4679b5238161 (patch)
tree2fff532e687a8e82543044352aeaf3168434aac1 /kernel/genOpcodeFiles.ml
parent3244b9c6e4159042bae0cd2ad48aba77928d7b2d (diff)
parent0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (diff)
Merge PR #11604: Primitive persistent arrays
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: proux01 Ack-by: silene
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
-rw-r--r--kernel/genOpcodeFiles.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 0a9f137c45..67a672c349 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -157,6 +157,10 @@ let opcodes =
"CHECKLDSHIFTEXP";
"CHECKNEXTUPFLOAT";
"CHECKNEXTDOWNFLOAT";
+ "ISINT_CAML_CALL2";
+ "ISARRAY_CAML_CALL1";
+ "ISARRAY_INT_CAML_CALL2";
+ "ISARRAY_INT_CAML_CALL3";
"STOP"
|]