aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* make display (freeze, ladderstep with adc)Gravatar Jason Gross2017-05-17
* Add compiler optimization for add-with-carryGravatar Jason Gross2017-05-17
* make display (with adc, bool)Gravatar Jason Gross2017-05-17
* Allow 'bool' in outputGravatar Jason Gross2017-05-17
* Add notations for adcGravatar Jason Gross2017-05-17
* make displayGravatar Jason Gross2017-05-17
* Zselect notationGravatar Jason Gross2017-05-17
* Add reflective machinery for adc, zselectGravatar Jason Gross2017-05-17
* Ltac scope interprets some notations as errors, so we make anf a definitionGravatar Jason Gross2017-05-17
* Fix a typo in prev commit, add convenience notationGravatar Jason Gross2017-05-17
* Allow specifying pipeline options at call-timeGravatar Jason Gross2017-05-17
* Update adc lemmas to version freeze actually usesGravatar Jason Gross2017-05-17
* Add more context proper lemmasGravatar Jason Gross2017-05-16
* Flip argument order on interp for easier Proper lemmasGravatar Jason Gross2017-05-16
* Add context_equiv and prove some Proper lemmasGravatar Jason Gross2017-05-16
* Revert "Add dec_eq_positive"Gravatar Jason Gross2017-05-16
* Add dec_eq_positiveGravatar Jason Gross2017-05-16
* Flip order of extendb, lookup argumentsGravatar Jason Gross2017-05-16
* Remove useless argumentGravatar Jason Gross2017-05-16
* Add Interp_compileGravatar Jason Gross2017-05-16
* Slightly better type for Interp_InterpToPHOASGravatar Jason Gross2017-05-16
* Add Named.ExprInversionGravatar Jason Gross2017-05-15
* Add Wf_from_unitGravatar Jason Gross2017-05-15
* Add more pointed prop lemmasGravatar Jason Gross2017-05-15
* Add src/Compilers/Z/Named/DeadCodeEliminationInterp.vGravatar Jason Gross2017-05-15
* Add DeadCodeEliminationInterpGravatar Jason Gross2017-05-15
* Add a stronger lemma to registerassigninterpGravatar Jason Gross2017-05-15
* use ladderstep from donna (2% faster?)Gravatar Andres Erbsen2017-05-15
* disable ANormal form, we now support expression output!Gravatar Andres Erbsen2017-05-14
* Add reserved java notationGravatar Jason Gross2017-05-14
* Add a reserved C notationGravatar Jason Gross2017-05-14
* update c.sh for new return notationGravatar Andres Erbsen2017-05-14
* Merge branch 'with-return' of https://github.com/JasonGross/fiat-crypto into ...Gravatar Andres Erbsen2017-05-14
|\
* | Add GetNamesGravatar Jason Gross2017-05-14
* | Add Named.default_names_forGravatar Jason Gross2017-05-14
| * make display (for return statement)Gravatar Jason Gross2017-05-14
| * Stick 'return' at the end of printed functionsGravatar Jason Gross2017-05-14
|/
* make display again (really not sure what's up)Gravatar Jason Gross2017-05-14
* make displayGravatar Jason Gross2017-05-14
* Add Named.CountLetsGravatar Jason Gross2017-05-14
* force carry intermediates to be bound earlyGravatar Andres Erbsen2017-05-14
* make display (ladderstep with specialize square)Gravatar Jason Gross2017-05-14
* Use specialized square in ladderstepGravatar Jason Gross2017-05-14
* Make proj1_sig square_sig take only one argumentGravatar Jason Gross2017-05-14
* Add Z/Named/DeadCodeElimination.vGravatar Jason Gross2017-05-14
* Split off EliminateDeadCodeGravatar Jason Gross2017-05-14
* make display without 0x0 * _Gravatar Jason Gross2017-05-14
* Do more arithmetic simplifyingGravatar Jason Gross2017-05-14
* specialize squaring earlierGravatar Andres Erbsen2017-05-14
* preserve common subexpressions in donna-derived codeGravatar Andres Erbsen2017-05-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 17:42:50 +0000