diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-01 19:16:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-01 19:37:41 +0200 |
| commit | cf5baeccf3cf7c24ccc69aa728bfe836fba5230a (patch) | |
| tree | 4e530c6ef169bd61bab7f30098d544947e8d7431 /kernel/byterun | |
| parent | ad66acf99a85cf1dee3bb56f70121130c090b0c4 (diff) | |
| parent | 4c66c7f9c370d2088dfa064e77f45b869c672e98 (diff) | |
Merge branch 'v8.5'
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++); } |