aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/BarrettReduction/Generalized.v
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
* 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
* rename-everythingGravatar Andres Erbsen2017-04-06