diff options
| author | Guillaume Melquiond | 2020-12-27 10:36:31 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-01-10 10:24:10 +0100 |
| commit | d009572893913b889320f2fa3435543ee4c63f82 (patch) | |
| tree | f15d2920bb65b888f6c21754b3cd9ee2c9723bcf /kernel/byterun/coq_fix_code.c | |
| parent | 723440611965ccdecfd56e61c8f1f8618a08841d (diff) | |
Remove PUSHACC0, as it is strictly equivalent to PUSH.
Diffstat (limited to 'kernel/byterun/coq_fix_code.c')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 1ba6a8c8fe..f562c15aa8 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -31,7 +31,8 @@ int arity[STOP+1]; void init_arity () { /* instruction with zero operand */ arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]= - arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]= + arity[ACC6]=arity[ACC7]= + arity[PUSH]=arity[PUSHACC1]= arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]= arity[PUSHACC6]=arity[PUSHACC7]= arity[ENVACC0]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]= |