aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-08-30 09:12:17 +0200
committerGuillaume Melquiond2020-11-13 15:13:23 +0100
commitaebc10aab3581a0561f96de6b5db6d530a65e658 (patch)
treefc77c92a0e39e4f77c4600ea4dc9e51f20a247b6 /kernel/byterun
parentfdd16113a042170022dce276e53e7a3308c0451c (diff)
Remove some unused opcodes from VM.
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_fix_code.c2
-rw-r--r--kernel/byterun/coq_interp.c14
2 files changed, 1 insertions, 15 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index cd431dbf2e..1ffb323748 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -43,7 +43,7 @@ void init_arity () {
arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
- arity[ISINT]=arity[AREINT2]=0;
+ 0;
/* instruction with one operand */
arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 74eb4973d0..67e6bed0d9 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1558,20 +1558,6 @@ value coq_interprete
Next;
}
- Instruct (ISINT){
- print_instr("ISINT");
- accu = (Is_uint63(accu)) ? coq_true : coq_false;
- Next;
- }
-
- Instruct (AREINT2){
- print_instr("AREINT2");
- accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false;
- sp++;
- Next;
- }
-
-
Instruct (CHECKOPPFLOAT) {
print_instr("CHECKOPPFLOAT");
CheckFloat1();