aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
Commit message (Expand)AuthorAge
* More zsimplifyGravatar Jason Gross2016-08-03
* Add some autogenerated zsimplify lemmasGravatar Jason Gross2016-08-03
* Better Zmod manipulationGravatar Jason Gross2016-08-03
* Weaken some ZUtil assumptionsGravatar Jason Gross2016-08-03
* More ZUtilGravatar Jason Gross2016-08-03
* More ZUtilGravatar Jason Gross2016-08-03
* Add ZUtil lemmas, and Util.BoolGravatar Jason Gross2016-08-03
* More zsimplify hintsGravatar Jason Gross2016-08-03
* Add {push,pull}_Zdiv databasesGravatar Jason Gross2016-08-03
* Add more ZUtil lemmasGravatar Jason Gross2016-08-03
* Add some simplification lemmas to ZUtilGravatar Jason Gross2016-08-02
* Add pull_Zmod tacticGravatar Jason Gross2016-08-01
* Make Z.ltb_to_lt more powerfulGravatar Jason Gross2016-08-01
* Add div lower/upper bounds to zarith hint dbGravatar Jason Gross2016-08-01
* Better hint for div_to_inv_moduloGravatar Jason Gross2016-08-01
* Add a lemma about removing division in modular arithmeticGravatar Jason Gross2016-08-01
* Fixes for Coq 8.4Gravatar Jason Gross2016-08-01
* Add [0 mod _ = 0] to zsimplify dbGravatar Jason Gross2016-08-01
* Add push_Zmod tacticsGravatar Jason Gross2016-07-29
* Don't give equiv_modulo reflexive instance priority over eqGravatar Jason Gross2016-07-29
* Add more Z.modulo lemmasGravatar Jason Gross2016-07-29
* Add another ZUtil rewrite hintGravatar Jason Gross2016-07-29
* Add a ZUtil rewrite hintGravatar Jason Gross2016-07-29
* Add equiv_modulo rewrite instancesGravatar Jason Gross2016-07-29
* Add some lemmas and hints about ZmodGravatar Jason Gross2016-07-29
* Add a zutil lemmaGravatar Jason Gross2016-07-29
* Add instances about congruence moduloGravatar Jason Gross2016-07-28
* Add Z.mod_mod to zsimplifyGravatar Jason Gross2016-07-28
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Restore functionality of Z.simplify_fractions_leGravatar Jason Gross2016-07-27
* Make Z.pre_reorder_fractions / Z.simplify_fractions_le not loopGravatar Jason Gross2016-07-27
* Add another ZUtil lemmaGravatar Jason Gross2016-07-26
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-25
|\
* | A couple new util lemmasGravatar jadep2016-07-25
| * More Zpow in ZUtilGravatar Jason Gross2016-07-22
| * More ZUtilGravatar Jason Gross2016-07-22
| * More ZUtil lemmasGravatar Jason Gross2016-07-22
| * Revert "Revert "Add more ZUtil automation""Gravatar Jason Gross2016-07-22
| * Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
| * Revert "Add more ZUtil automation"Gravatar Jason Gross2016-07-22
| * Add more ZUtil automationGravatar Jason Gross2016-07-22
| * Generalize div_sub_small a bitGravatar Jason Gross2016-07-22
|/
* Add another lemma to zarithGravatar Jason Gross2016-07-21
* Add another ZUtil lemmaGravatar Jason Gross2016-07-21
* Another ZUtil lemmaGravatar Jason Gross2016-07-21
* Fix broken proofsGravatar Jason Gross2016-07-21
* Add more ZUtilGravatar Jason Gross2016-07-21
* More ZUtil helper lemmasGravatar Jason Gross2016-07-21
* Add more ZUtil lemmasGravatar Jason Gross2016-07-21
* Add ZUtil lemmasGravatar Jason Gross2016-07-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 16:42:00 +0000