| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès | |
| 2018-03-03 | Handling evars in the VM. | Pierre-Marie Pédrot | |
| We simply treat them as as an application of an atom to its instance, and in the decompilation phase we reconstruct the instance from the stack. This grants wish BZ#5659. | |||
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2018-02-23 | New IR in VM: Clambda. | Maxime Dénès | |
| 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 formal proof system |
| aboutsummaryrefslogtreecommitdiff |