aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* 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
* WIP castGravatar Jason Gross2018-03-19
* Update montred to newish pipeline, revive DCEGravatar Jason Gross2018-03-19
* Add a ring goalGravatar Jason Gross2018-03-19
* subsetoid_ring: don't ask for false thingsGravatar Jason Gross2018-03-12
* Add Algebra.SubsetoidRingGravatar Jason Gross2018-03-12
* Review comments.Gravatar David Benjamin2018-03-09
* easy bitsGravatar David Benjamin2018-03-09
* Prove another Barrett reduction variant.Gravatar David Benjamin2018-03-09
* Don't use deprecated compat notations in ZUtilGravatar Jason Gross2018-03-07
* Add comments about [refresh] failingGravatar Jason Gross2018-03-07
* actually reprint montgomery and uncomment a couple notations -- should have b...Gravatar Jade Philipoom2018-03-07
* fix a typo, some comments, and notationsGravatar Jade Philipoom2018-03-07
* make Montgomery do associational carries in a generalized wayGravatar Jade Philipoom2018-03-07
* remove special-case convert-mul-convert implementation and use generalized on...Gravatar Jade Philipoom2018-03-07
* remove unneeded, commented-out codeGravatar Jade Philipoom2018-03-07
* Add a dummy length argument to make partial evaluation work (see #321) and fi...Gravatar Jade Philipoom2018-03-07
* factor out convert-mul-convert and prove correctnessGravatar Jade Philipoom2018-03-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 11:11:31 +0000