aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic
Commit message (Expand)AuthorAge
* partition -> Partition.partition to prevent confusion with List.partitionGravatar jadep2019-04-03
* remove unnecessary imports from Primitives.vGravatar jadep2019-04-03
* remove extraneous module identifiersGravatar jadep2019-04-03
* update _CoqProject, fix indentations, and prune dependencies of new Arithmeti...Gravatar jadep2019-04-03
* split up Arithmetic (imports etc. not yet fixed, does not build)Gravatar jadep2019-04-03
* Get new Barrett proofs to generate Fancy code as beforeGravatar jadep2019-03-25
* remove old pipelineGravatar Andres Erbsen2019-01-09
* Fix bugs introduced by previous commitGravatar Jason Gross2018-12-04
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Backwards compatible fix for some issues from https://github.com/coq/coq/pull...Gravatar Jason Gross2018-08-04
* 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
* Fix naming issueGravatar Jade Philipoom2018-02-23
* add equivalence proof for Montgomery reduce_via_partial_altGravatar Jade Philipoom2018-02-23
* Add MontgomeryAPI.encode and two lemmas about itGravatar Jason Gross2017-11-14
* fix commentGravatar jadep2017-11-12
* Fix another side condition issueGravatar Jason Gross2017-11-08
* Fix a bug in previous commitGravatar Jason Gross2017-11-08
* Add freeze rewrite lemmas to dbsGravatar Jason Gross2017-11-08
* Add karatsuba, goldilocks lemmas to rewrite dbsGravatar Jason Gross2017-11-07
* Move chained_carries' (now chained_carries_reduce)Gravatar Jason Gross2017-11-07
* Add more versions of basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-11-07
* Split off computational part of basesystem_partial_evaluation_RHS_genGravatar Jason Gross2017-11-07
* More use of Z.eqb_cpsGravatar Jason Gross2017-11-07
* Use div_cps and modulo_cps in more placesGravatar Jason Gross2017-11-07
* Make use of id_tuple_with_alt_cps'Gravatar Jason Gross2017-11-06
* Make use of from_associational_cps in more placesGravatar Jason Gross2017-11-01
* More use of Z.eqb_cpsGravatar Jason Gross2017-11-01
* Add another unfolding databaseGravatar Jason Gross2017-10-22
* Fix bug in previous commitGravatar Jason Gross2017-10-20
* Use div_cps, modulo_cpsGravatar Jason Gross2017-10-20
* Use fold_right_cps2 to get eqb_cps to get the right continuation typeGravatar Jason Gross2017-10-19
* Add more unfolds to basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-10-19
* Switch arithmetic to cps for Z * Z under the hoodGravatar Jason Gross2017-10-19
* Move tactics around in src/Arithmetic/CoreUnfolder.vGravatar Jason Gross2017-10-19
* Pattern over cps lemmas in Arithmetic/CoreGravatar Jason Gross2017-10-19
* Unfold more things in basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-10-18
* Add some more things to basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-10-18
* Add basesystem_partial_evaluation_unfolder dbGravatar Jason Gross2017-10-18
* Unfold more things in core unfolderGravatar Jason Gross2017-10-18
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-18
* Pattern more things in arithmetic/coreGravatar Jason Gross2017-10-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 10:48:11 +0000