diff options
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index bf383a33a..df5fdce75 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -903,10 +903,12 @@ value coq_interprete Alloc_small(block, 2, ATOM_PROJ_TAG); Field(block, 0) = Field(coq_global_data, *pc); Field(block, 1) = accu; - /* Create accumulator */ - Alloc_small(accu, 2, Accu_tag); - Code_val(accu) = accumulate; - Field(accu, 1) = block; + accu = block; + /* Create accumulator */ + Alloc_small(block, 2, Accu_tag); + Code_val(block) = accumulate; + Field(block, 1) = accu; + accu = block; } else { accu = Field(accu, *pc++); } |