| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-11-01 | Implement classify on primitive float | Pierre Roux | |
| 2019-11-01 | Add primitive floats to 'vm_compute' | Guillaume Bertholon | |
| * This commit add float instructions to the VM, their encoding in bytecode and the interpretation of primitive float values after the reduction. * The flag '-std=c99' could be added to the C compiler flags to ensure that float computation strictly follows the norm (ie. i387 80-bits format is not used as an optimization). Actually, we use '-fexcess-precision=standard' instead of '-std=c99' because the latter would disable GNU asm used in the VM. | |||
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann | |
| 2019-03-01 | [Kernel] Simpler generation of opcode files | Vincent Laporte | |
| Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program rather than a pipeline of sed and awk text processing. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |