aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* remove old loops codeGravatar Andres Erbsen2018-03-27
* cleanup2Gravatar Andres Erbsen2018-03-27
* cleanupGravatar Andres Erbsen2018-03-27
* comprehensiveGravatar Andres Erbsen2018-03-27
* tail recursionGravatar Andres Erbsen2018-03-27
* refactor measureGravatar Andres Erbsen2018-03-27
* prove iffGravatar Andres Erbsen2018-03-27
* wip completeness proofGravatar Andres Erbsen2018-03-27
* work on completeness of measure analysisGravatar Andres Erbsen2018-03-27
* loops: more lemmasGravatar Andres Erbsen2018-03-27
* cpsloopsGravatar Andres Erbsen2018-03-27
* Response to code review commentGravatar Jason Gross2018-03-23
* Be more explicit about reductionGravatar Jason Gross2018-03-23
* s/nobrainer1/subst01/Gravatar Jason Gross2018-03-23
* Remove spurious indentationGravatar Jason Gross2018-03-23
* Added input var type for clarityGravatar Jason Gross2018-03-23
* Make the ERROR definition opaque to vm_computeGravatar Jason Gross2018-03-23
* Add GeneralizeVar explanatory commentGravatar Jason Gross2018-03-23
* Flip the meaning of a boolean testGravatar Jason Gross2018-03-23
* Add a comment explaining default inhabitantsGravatar Jason Gross2018-03-23
* Use nobrainer1 in the pipelineGravatar Jason Gross2018-03-23
* Add NoBrainer1Gravatar Jason Gross2018-03-23
* Thunk let-bound default values, unfold bool_rectGravatar Jason Gross2018-03-23
* Update output of montred from the dlet place changeGravatar Jason Gross2018-03-22
* [experiments] Remove dead code, inline some thingsGravatar Jason Gross2018-03-22
* Add another reserved notation for App_fstGravatar Jason Gross2018-03-21
* s/partial reduction/partial evaluation/Gravatar Jason Gross2018-03-21
* Don't inline var nodes on the first pass through partial evaluationGravatar Jason Gross2018-03-21
* Let-bind placeGravatar Jason Gross2018-03-21
* [experiments] Thunk the eliminator casesGravatar Jason Gross2018-03-20
* Remove some dead codeGravatar Jason Gross2018-03-19
* Fix for Coq <= 8.7Gravatar Jason Gross2018-03-19
* Add support for Z*Z casts, get montred workingGravatar Jason Gross2018-03-19
* Split up the two calls to `lazy`Gravatar Jason Gross2018-03-19
* Fix some bugs in cachingGravatar Jason Gross2018-03-19
* Add comments explaining the various [interp] functionsGravatar Jason Gross2018-03-19
* Add commented out example of using the full end-to-end lemma inlineGravatar Jason Gross2018-03-19
* Add end-to-end correctness lemmaGravatar Jason Gross2018-03-19
* Unify cache and nocacheGravatar Jason Gross2018-03-19
* Add alternate tactics for handling the all-in-one-derive caseGravatar Jason Gross2018-03-19
* Clean and simplify some codeGravatar Jason Gross2018-03-19
* WIP with Andres on cleaning boilerplateGravatar Jason Gross2018-03-19
* Partial fix for montredGravatar Jason Gross2018-03-19
* Speed up the final pipeline by about 2xGravatar Jason Gross2018-03-19
* Insert missing commentGravatar Jason Gross2018-03-19
* Remove dead bounds analysis codeGravatar Jason Gross2018-03-19
* Move the ring goal upGravatar Jason Gross2018-03-19
* Add shiftl notationGravatar Jason Gross2018-03-19
* Update printingGravatar Jason Gross2018-03-19
* Move relax_zrange to a separate phaseGravatar Jason Gross2018-03-19