aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/Conversions.v
Commit message (Expand)AuthorAge
* Refactors to remove intermediate conversionsGravatar Robert Sloan2016-10-26
* Refactors to remove intermediate conversions in HLConversionsGravatar Robert Sloan2016-10-25
* More Coq 8.4 fixesGravatar Jason Gross2016-10-22
* Merge branch 'master' into pr/84Gravatar Jason Gross2016-10-22
|\
| * Interpret LetIn to Let_In for better control of interpGravatar Jason Gross2016-10-22
* | Make lower bounds work by using HL conversionsGravatar Robert Sloan2016-10-21
* | committing unstable refactors to patch masterGravatar Robert Sloan2016-10-21
| * Various fixes for Coq 8.4Gravatar Jason Gross2016-10-20
|/
* Fast bounds-checking machinery but lower-bounds are brokenGravatar Robert Sloan2016-10-18
* Converting to bounded machineryGravatar Robert Sloan2016-10-17
* More of the Conversions.v correctness proofsGravatar Robert Sloan2016-10-14
* Making sub bounds actually tightGravatar Robert Sloan2016-10-14
* More minor improvements in Conversions.v and Compile.vGravatar Robert Sloan2016-10-13
* Minor refactors waiting for the code generation to finishGravatar Robert Sloan2016-10-13
* Minor refactors waiting for the code generation to finishGravatar Robert Sloan2016-10-13
* Complete example + GF25519 outline in Pipeline.vGravatar Robert Sloan2016-10-02
* Most of our refactored compilation infrastructureGravatar Rob Sloan2016-10-02
* Large-scale refactoring of src/AssemblyGravatar Robert Sloan2016-09-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 14:44:55 +0000