From d009572893913b889320f2fa3435543ee4c63f82 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 27 Dec 2020 10:36:31 +0100
Subject: Remove PUSHACC0, as it is strictly equivalent to PUSH.

---
 kernel/byterun/coq_fix_code.c | 3 ++-
 kernel/byterun/coq_interp.c   | 4 ----
 2 files changed, 2 insertions(+), 5 deletions(-)

(limited to 'kernel/byterun')

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;
-- 
cgit v1.2.3