aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
...
* 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
| | * Add a NatUtil lemma and dbGravatar Jason Gross2016-07-08
| | * Add a ListUtil lemmaGravatar Jason Gross2016-07-08
| | * Add a ListUtil lemmaGravatar Jason Gross2016-07-08
| | * Add Z.div_0_l to ZUtilGravatar Jason Gross2016-07-08
| | * Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-08
* | | Util/Tuple: added a version of from_list that doesn't require a proof of leng...Gravatar jadep2016-07-08
| * | Util/Tuple: added a version of from_list that doesn't require a proof of leng...Gravatar jadep2016-07-08
| * | Added mod case to zero_boundsGravatar jadep2016-07-08
| | * Add update_nth out of boundsGravatar Jason Gross2016-07-07
| | * Add hint db in ListUtilGravatar Jason Gross2016-07-07
| | * More ListUtil factsGravatar Jason Gross2016-07-07
| | * Slightly better arguments in ListUtilGravatar Jason Gross2016-07-07
| | * Correct hintdb namesGravatar Jason Gross2016-07-07
| | * Add more about firstn to listutilGravatar Jason Gross2016-07-07
| | * Add more update_nth to ListUtilGravatar Jason Gross2016-07-07
| | * Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-07
| | * Add pow2_mod to ZUtilGravatar Jason Gross2016-07-07
| |/
| * Fix notations, add &Gravatar Jason Gross2016-07-06
| * Add [update_nth] to ListUtil, change [set_nth]Gravatar Jason Gross2016-07-06
| * Add notations for Z.shift{r,l} to ZUtilGravatar Jason Gross2016-07-06
| * Improve some reserved notationsGravatar Jason Gross2016-07-06
| * Fix for broken 8.5 build in ListUtilGravatar Jason Gross2016-07-06
| * fixed indentation for new lemmas in ZUtilGravatar jadep2016-07-06
| * Merged changes, including new ZUtil conventions.Gravatar jadep2016-07-06
| |\
| * \ Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-07-06
| |\ \
| * | | Factored out some proofs that rely only on base being powers of two, and defi...Gravatar jadep2016-07-06
* | | | stuck trying to figure out dependently typed continuation passing styleGravatar Andres Erbsen2016-07-06
* | | | Tuple: lift functions from lists to tuplesGravatar Andres Erbsen2016-07-03
| | | * Indentation in ZUtilGravatar Jason Gross2016-07-02
| | | * Make ZUtil more uniformGravatar Jason Gross2016-07-02
| |_|/ |/| |
* | | Fix for 8.4 evarsGravatar Jason Gross2016-07-01
* | | Add ZUtil hintsGravatar Jason Gross2016-07-01
* | | Add more hints to ZUtilGravatar Jason Gross2016-07-01
* | | Add more hints in ZUtilGravatar Jason Gross2016-07-01
* | | Add more ZUtil hintsGravatar Jason Gross2016-07-01
* | | Add more hints to ZUtilGravatar Jason Gross2016-07-01
* | | Add hint databases and a proof about Z.log2Gravatar Jason Gross2016-07-01