diff options
| author | Pierre-Marie Pédrot | 2018-05-28 20:11:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-28 20:11:06 +0200 |
| commit | a205bb9f2a93396aad154ec50f6f122cbd46811c (patch) | |
| tree | cd1ad9834fa9e6391193b377cc4533f9eba702c5 /kernel/byterun | |
| parent | 81535edc4b21015bd63d23e57ca9d707b4b71f6b (diff) | |
| parent | 131ac2af3778a741f5f33e212ef4a57f7a91d20a (diff) | |
Merge PR #7521: Fix soundness bug with VM/native and cofixpoints
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 8ac1ecc79e..a944dbb06c 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1032,7 +1032,7 @@ value coq_interprete CHECK_STACK(nargs+1); sp -= nargs; for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); - *--sp = accu; // Last argument is the pointer to the suspension + *--sp = accu; // Leftmost argument is the pointer to the suspension print_lint(nargs); coq_extra_args = nargs; pc = Code_val(coq_env); // Trigger evaluation |