aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/BarrettReduction
Commit message (Expand)AuthorAge
* Get new Barrett proofs to generate Fancy code as beforeGravatar jadep2019-03-25
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* Make all parameters implicitGravatar Jasper Hugunin2018-07-02
* remove commentGravatar Jade Philipoom2018-04-11
* add a comment to rerun buildGravatar Jade Philipoom2018-04-11
* Automate some proofs a bit moreGravatar Jason Gross2018-04-11
* try to fix build on coq masterGravatar Jade Philipoom2018-04-11
* prove stronger bound on quotient error for barrett reductionGravatar Jade Philipoom2018-04-11
* Review comments.Gravatar David Benjamin2018-03-09
* easy bitsGravatar David Benjamin2018-03-09
* Prove another Barrett reduction variant.Gravatar David Benjamin2018-03-09
* rename-everythingGravatar Andres Erbsen2017-04-06