| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | [lib] Move global options to their proper place. |  Emilio Jesus Gallego Arias | 2018-04-02 |
| | | | | | | | | | Recent commits introduced global flags, but these should be module-specific so relocating. Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced to the truly global stuff. | ||
| * | New IR in VM: Clambda. |  Maxime Dénès | 2018-02-23 |
| This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |