aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Allow loop notation to printGravatar Jason Gross2017-06-05
* Make Karatsuba depend on Arithmetic/Core to make calling it less of a painGravatar jadep2017-06-02
* export a few more wrapper definitions in PositionalGravatar jadep2017-06-02
* first successful stage of karatsuba synthesisGravatar jadep2017-06-02
* pulled in a CPS version of Karatsuba from another branchGravatar jadep2017-06-02
* Add an only-parsing loop notationGravatar Jason Gross2017-06-02
* Add experimental loopsGravatar Jason Gross2017-06-02
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* Only use bool in freezeGravatar Jason Gross2017-05-21
* fix last wide mul in curve25519-51Gravatar Andres Erbsen2017-05-20
* src/Specific/x25519_c64.c.sh: use exact donna skeletonGravatar Andres Erbsen2017-05-20
* make displayGravatar Jason Gross2017-05-20
* Fix extra opp in freezeGravatar Jason Gross2017-05-20
* make display (freeze, fully notationified)Gravatar Jason Gross2017-05-20
* Add compiler optimization for [Zselect (-x) _ _]Gravatar Jason Gross2017-05-20
* make displayGravatar Jason Gross2017-05-20
* Get sbb conversion working in the pipelineGravatar Jason Gross2017-05-20
* make displayGravatar Jason Gross2017-05-20
* Add adc -> sbb to arithmetic simpliferGravatar Jason Gross2017-05-20
* Add sbb notations to CNotationsGravatar Jason Gross2017-05-20
* Also reify Z.sub_with_get_borrowGravatar Jason Gross2017-05-20
* Add SubWithGetBorrow to reflective machineryGravatar Jason Gross2017-05-20
* Add InlineConstAndOppGravatar Jason Gross2017-05-19
* Add subst_prod tactic to Prod.vGravatar Jason Gross2017-05-19
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 00:25:45 +0000