diff options
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 4bc6848ba7..2c0b580e24 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -70,7 +70,9 @@ void init_arity () { arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]= - arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; + arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]= + arity[CHECKNEXTUPFLOATINPLACE]=arity[CHECKNEXTDOWNFLOATINPLACE]= + 1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]= |