aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* git submodule update --remote --recursiveGravatar Andres Erbsen2018-02-24
* coqprime in COQPATH (closes #269)Gravatar Andres Erbsen2018-02-24
* Add ZRange.intersectionGravatar Jason Gross2018-02-23
* Fix a typoGravatar Jason Gross2018-02-23
* Add some bounds operations to ZRangeGravatar Jason Gross2018-02-23
* Add ZRange.oppGravatar Jason Gross2018-02-23
* Make the Montgomery reduction test case use 128-bit multiplications andGravatar Jade Philipoom2018-02-23
* fix leftover %RTGravatar Jade Philipoom2018-02-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 19:26:16 +0000