aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers
Commit message (Expand)AuthorAge
...
* Stronger invert_op tacticGravatar Jason Gross2017-06-13
* Fix a major bug in C-notation printingGravatar Jason Gross2017-06-13
* Reify Z.mul_with_split_at_bitwidthGravatar Jason Gross2017-06-13
* Handle IdWithAlt in the simplifierGravatar Jason Gross2017-06-12
* Add some more constant notationsGravatar Jason Gross2017-06-12
* Push bounds side conditions through the pipelineGravatar Jason Gross2017-06-12
* Add CompileInterpSideConditions.vGravatar Jason Gross2017-06-12
* Add snd_interpf_side_conditions_gen_SomeGravatar Jason Gross2017-06-12
* Add Named.InterpSideConditionsGravatar Jason Gross2017-06-12
* Add Z.InterpSideConditionsGravatar Jason Gross2017-06-12
* Add InterpSideConditionsGravatar Jason Gross2017-06-12
* Have interped_op_side_conditions return a pointed_PropGravatar Jason Gross2017-06-12
* Initial stab at id_with_altGravatar Jason Gross2017-06-11
* Add dummy version of IdWithAlt to compilersGravatar Jason Gross2017-06-11
* Be more forceful about clearing before abstract in glue codeGravatar Jason Gross2017-06-11
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Only use bool in freezeGravatar Jason Gross2017-05-21
* Fix extra opp in freezeGravatar Jason Gross2017-05-20
* Add compiler optimization for [Zselect (-x) _ _]Gravatar Jason Gross2017-05-20
* Get sbb conversion working in the pipelineGravatar 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 compiler optimization for add-with-carryGravatar Jason Gross2017-05-17
* Allow 'bool' in outputGravatar Jason Gross2017-05-17
* Add notations for adcGravatar 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
* 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
* 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 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
* 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
* Merge branch 'with-return' of https://github.com/JasonGross/fiat-crypto into ...Gravatar Andres Erbsen2017-05-14
|\
* | Add GetNamesGravatar Jason Gross2017-05-14