diff options
Diffstat (limited to 'kernel/byterun/coq_interp.c')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 216919ae3..84bc08d2b 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -922,26 +922,6 @@ value coq_interprete } /* Special operations for reduction of open term */ - Instruct(ACCUMULATECOND) { - int i, num; - print_instr("ACCUMULATECOND"); - num = *pc; - pc++; - if (Field(coq_global_boxed, num) == Val_false || coq_all_transp) { - /* printf ("false\n"); - printf ("tag = %d", Tag_val(Field(accu,1))); */ - num = Wosize_val(coq_env); - for(i = 2; i < num; i++) *--sp = Field(accu,i); - coq_extra_args = coq_extra_args + (num - 2); - coq_env = Field(Field(accu,1),1); - pc = Code_val(coq_env); - accu = coq_env; - /* printf ("end\n"); */ - Next; - }; - /* printf ("true\n"); */ - } - Instruct(ACCUMULATE) { mlsize_t i, size; print_instr("ACCUMULATE"); |