aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/FancyMachine256
Commit message (Expand)AuthorAge
* Flip argument order on interp for easier Proper lemmasGravatar Jason Gross2017-05-16
* Add DeadCodeEliminationInterpGravatar Jason Gross2017-05-15
* CSE without inlining arithmetic expressionsGravatar Jason Gross2017-05-14
* Support destructuring dlet and sletGravatar Jason Gross2017-05-13
* Split off a-normal form from flatteningGravatar Jason Gross2017-04-14
* Add support for cse-modulo-normalizationGravatar Jason Gross2017-04-14
* Split off Compilers.Named.ContextGravatar Jason Gross2017-04-10
* rename-everythingGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Add Wf_InterpToPHOASGravatar Jason Gross2017-03-14
* Move ContextOk to ContextDefinitionsGravatar Jason Gross2017-03-14
* Remove stuff from Reflection/Named/SyntaxGravatar Jason Gross2017-03-08
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Add syntactic tuplesGravatar Jason Gross2016-11-06
* Add support for dependent reificationGravatar Jason Gross2016-11-06
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* Split up DoubleBoundedProofs, add proofsGravatar Jason Gross2016-10-07
* Add bitwise and, remove mkl from fancyGravatar Jason Gross2016-10-03
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-10-03
* Drop CSE from Fancy MachineGravatar Jason Gross2016-09-22
* Use dlet, not lletGravatar Jason Gross2016-09-22
* Don't inline everything in Montgomery and BarrettGravatar Jason Gross2016-09-22
* Make use of named syntax, do reg assign for fancyGravatar Jason Gross2016-09-22
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Move FancyMachine from Experiments to SpecificGravatar Jason Gross2016-09-08