| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-26 | Make it more obvious when the calling convention of APPLY changes. | Guillaume Melquiond | |
| Despite their names, APPLY1 to APPLY4 are completely different from APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return address was already pushed on the stack, before the arguments were. On the other hand, APPLY1 to APPLY4 insert the return address in the middle of the already pushed arguments. | |||
| 2021-01-10 | Remove MAKEPROD. | Guillaume Melquiond | |
| MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is never encountered in the fast path, this optimization is not worth the extra complexity. | |||
| 2020-11-13 | Turn Ksequence into a unary opcode, as its binary structure was never used. | Guillaume Melquiond | |
| 2020-11-13 | Remove some unused opcodes from VM. | Guillaume Melquiond | |
| 2020-11-13 | Remove unchecked arithmetic operations from VM, as they are not used. | Guillaume Melquiond | |
| 2020-08-18 | Rename VM-related kernel/cfoo files to kernel/vmfoo | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |