aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Saturated/MontgomeryAPI.v
Commit message (Expand)AuthorAge
* 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
* Add MontgomeryAPI.encode and two lemmas about itGravatar Jason Gross2017-11-14
* Add more versions of basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-11-07
* Fix bug in previous commitGravatar Jason Gross2017-10-20
* Switch arithmetic to cps for Z * Z under the hoodGravatar Jason Gross2017-10-19
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
* Remove some admitted lemmasGravatar Jason Gross2017-07-07
* Closed under the global contextGravatar Andres Erbsen2017-07-02
* prove [MontgomeryAPI.small_add]Gravatar Andres Erbsen2017-07-02
* [small] admits progress...Gravatar Andres Erbsen2017-07-01
* change opp to runtime_oppGravatar jadep2017-07-01
* proved remaining [eval] admits in MontgomeryAPIGravatar jadep2017-07-01
* Prove saturated carrying-addition-chain correctGravatar jadep2017-06-30
* Reorganization of saturated arithmeticGravatar jadep2017-06-29