Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Add ZUtil lemmas | 2016-07-21 | ||
| | ||||
* | Add Z.lt_le_incl to zarith | 2016-07-20 | ||
| | ||||
* | Add another lemma about +, <= to arith | 2016-07-20 | ||
| | ||||
* | Add a distr_length database | 2016-07-19 | ||
| | ||||
* | Remove stuff from PseudoMersenneBaseParamProofs.v | 2016-07-19 | ||
| | ||||
* | Add a lemma about sum_firstn | 2016-07-18 | ||
| | ||||
* | Add a ListUtil lemma | 2016-07-18 | ||
| | ||||
* | Fix for Coq 8.4 (missing lemmas) | 2016-07-18 | ||
| | ||||
* | Fix for Coq 8.4 (omega used to be weaker) | 2016-07-18 | ||
| | ||||
* | Add more natsimplify le_dec lemmas | 2016-07-18 | ||
| | ||||
* | Add more NatUtil lemmas | 2016-07-18 | ||
| | ||||
* | Add natsimplify lemmas about eq_nat_dec | 2016-07-18 | ||
| | ||||
* | Fix some typos in the previous commit | 2016-07-18 | ||
| | ||||
* | Add some lemmas about nth_default in bounds | 2016-07-18 | ||
| | ||||
* | Move some definitions to Pow2Base (#24) | 2016-07-18 | ||
| | | | | | | | | | * Move some definitions to Pow2Base These definitions don't depend on PseudoMersenneBaseParams, only on limb_widths, and we'll want them for BarrettReduction / P256. * Fix for Coq 8.4 | |||
* | ported IterAssocOp to use monoid rather than a billion context variables ↵ | 2016-07-18 | ||
| | | | | that add up to a monoid | |||
* | Added lemmas to ZUtil and NatUtil (for Testbit) | 2016-07-18 | ||
| | ||||
* | tuple: applying functions to tuples of arbitrary length | 2016-07-12 | ||
| | ||||
* | Merge of fixedlength and master | 2016-07-11 | ||
|\ | ||||
| * | wrap nsatz in Algebra | 2016-07-11 | ||
| | | ||||
| * | [congruence] is more powerful in 8.5 than in 8.4 | 2016-07-11 | ||
| | | ||||
| * | merge | 2016-07-10 | ||
| |\ | ||||
| * | | added proofs about addition chain exponentiation for later use in ↵ | 2016-07-10 | ||
| | | | | | | | | | | | | ModularBaseSystem [pow], which we need for sqrt and inversion. | |||
| | * | Fix ListUtil for Coq 8.4 | 2016-07-10 | ||
| | | | ||||
| | * | Update ListUtil | 2016-07-08 | ||
| | | | ||||
| | * | Fix NatUtil for 8.4 | 2016-07-08 | ||
| | | | ||||
| | * | Add useful tactics and util lemmas | 2016-07-08 | ||
| | | | ||||
| | * | Add a NatUtil lemma and db | 2016-07-08 | ||
| | | | ||||
| | * | Add a ListUtil lemma | 2016-07-08 | ||
| | | | ||||
| | * | Add a ListUtil lemma | 2016-07-08 | ||
| | | | ||||
| | * | Add Z.div_0_l to ZUtil | 2016-07-08 | ||
| | | | ||||
| | * | Fix ListUtil for Coq 8.4 | 2016-07-08 | ||
| | | | | | | | | | | | | | | | [rewrite_strat] ignores [using tac] sometimes, and [Hint Rewrite] only accepts one database in 8.4. | |||
* | | | Util/Tuple: added a version of from_list that doesn't require a proof of ↵ | 2016-07-08 | ||
| | | | | | | | | | | | | length equality | |||
| * | | Util/Tuple: added a version of from_list that doesn't require a proof of ↵ | 2016-07-08 | ||
| | | | | | | | | | | | | length equality | |||
| * | | Added mod case to zero_bounds | 2016-07-08 | ||
| | | | ||||
| | * | Add update_nth out of bounds | 2016-07-07 | ||
| | | | ||||
| | * | Add hint db in ListUtil | 2016-07-07 | ||
| | | | ||||
| | * | More ListUtil facts | 2016-07-07 | ||
| | | | ||||
| | * | Slightly better arguments in ListUtil | 2016-07-07 | ||
| | | | ||||
| | * | Correct hintdb names | 2016-07-07 | ||
| | | | ||||
| | * | Add more about firstn to listutil | 2016-07-07 | ||
| | | | ||||
| | * | Add more update_nth to ListUtil | 2016-07-07 | ||
| | | | ||||
| | * | Fix ListUtil for Coq 8.4 | 2016-07-07 | ||
| | | | ||||
| | * | Add pow2_mod to ZUtil | 2016-07-07 | ||
| |/ | ||||
| * | Fix notations, add & | 2016-07-06 | ||
| | | ||||
| * | Add [update_nth] to ListUtil, change [set_nth] | 2016-07-06 | ||
| | | | | | | | | Define [set_nth] in terms of [update_nth] | |||
| * | Add notations for Z.shift{r,l} to ZUtil | 2016-07-06 | ||
| | | ||||
| * | Improve some reserved notations | 2016-07-06 | ||
| | | | | | | | | Compatibility with theories/Numbers/NatInt/NZBits.v | |||
| * | Fix for broken 8.5 build in ListUtil | 2016-07-06 | ||
| | | ||||
| * | fixed indentation for new lemmas in ZUtil | 2016-07-06 | ||
| | |