aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/FancyMachine256
Commit message (Expand)AuthorAge
* 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