diff options
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 14 |
2 files changed, 1 insertions, 15 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index ab6e393178..51ac290ad0 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -40,7 +40,7 @@ void init_arity () { arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[APPLY4]=arity[RESTART]= arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE1]= arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE1]= - arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]= + arity[GETFIELD0]=arity[GETFIELD1]= arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 62683b87a6..a1537cd963 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1011,20 +1011,6 @@ value coq_interprete Next; } - Instruct(SETFIELD0){ - print_instr("SETFIELD0"); - caml_modify(&Field(accu, 0),*sp); - sp++; - Next; - } - - Instruct(SETFIELD1){ - print_instr("SETFIELD1"); - caml_modify(&Field(accu, 1),*sp); - sp++; - Next; - } - Instruct(SETFIELD){ print_instr("SETFIELD"); caml_modify(&Field(accu, *pc),*sp); |