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 | |
| parent | 723440611965ccdecfd56e61c8f1f8618a08841d (diff) | |
Remove PUSHACC0, as it is strictly equivalent to PUSH.
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 3 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 4 |
2 files changed, 2 insertions, 5 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]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 6255250218..a124a51c7d 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -338,10 +338,6 @@ value coq_interprete print_instr("PUSH"); *--sp = accu; Next; } - Instruct(PUSHACC0) { - print_instr("PUSHACC0"); - *--sp = accu; Next; - } Instruct(PUSHACC1){ print_instr("PUSHACC1"); *--sp = accu; accu = sp[1]; Next; |