aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
...
* 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
* Fix 8.4 build.Gravatar jadep2016-07-25
* 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
| * Add reverse_nondep and ring_simplify_subterms_in_all tacticsGravatar 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
| * Add ring_simplify_subtermsGravatar 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
* Add Z.lt_le_incl to zarithGravatar Jason Gross2016-07-20
* Add another lemma about +, <= to arithGravatar Jason Gross2016-07-20
* Add a distr_length databaseGravatar Jason Gross2016-07-19
* Remove stuff from PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
* Add a lemma about sum_firstnGravatar Jason Gross2016-07-18
* Add a ListUtil lemmaGravatar Jason Gross2016-07-18
* Fix for Coq 8.4 (missing lemmas)Gravatar Jason Gross2016-07-18
* Fix for Coq 8.4 (omega used to be weaker)Gravatar Jason Gross2016-07-18
* Add more natsimplify le_dec lemmasGravatar Jason Gross2016-07-18
* Add more NatUtil lemmasGravatar Jason Gross2016-07-18
* Add natsimplify lemmas about eq_nat_decGravatar Jason Gross2016-07-18
* Fix some typos in the previous commitGravatar Jason Gross2016-07-18
* Add some lemmas about nth_default in boundsGravatar Jason Gross2016-07-18
* Move some definitions to Pow2Base (#24)Gravatar Jason Gross2016-07-18
* ported IterAssocOp to use monoid rather than a billion context variables that...Gravatar jadep2016-07-18
* Added lemmas to ZUtil and NatUtil (for Testbit)Gravatar jadep2016-07-18
* tuple: applying functions to tuples of arbitrary lengthGravatar Andres Erbsen2016-07-12
* Merge of fixedlength and masterGravatar jadep2016-07-11
|\
| * wrap nsatz in AlgebraGravatar Andres Erbsen2016-07-11
| * [congruence] is more powerful in 8.5 than in 8.4Gravatar Andres Erbsen2016-07-11
| * mergeGravatar jadep2016-07-10
| |\
| * | added proofs about addition chain exponentiation for later use in ModularBase...Gravatar jadep2016-07-10
| | * Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-10
| | * Update ListUtilGravatar Jason Gross2016-07-08
| | * Fix NatUtil for 8.4Gravatar Jason Gross2016-07-08
| | * Add useful tactics and util lemmasGravatar Jason Gross2016-07-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-26 08:26:34 +0000