fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
*	Add ZUtil lemmas	Jason Gross	2016-07-21
*	Add Z.lt_le_incl to zarith	Jason Gross	2016-07-20
*	Add another lemma about +, <= to arith	Jason Gross	2016-07-20
*	Add a distr_length database	Jason Gross	2016-07-19
*	Remove stuff from PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
*	Add a lemma about sum_firstn	Jason Gross	2016-07-18
*	Add a ListUtil lemma	Jason Gross	2016-07-18
*	Fix for Coq 8.4 (missing lemmas)	Jason Gross	2016-07-18
*	Fix for Coq 8.4 (omega used to be weaker)	Jason Gross	2016-07-18
*	Add more natsimplify le_dec lemmas	Jason Gross	2016-07-18
*	Add more NatUtil lemmas	Jason Gross	2016-07-18
*	Add natsimplify lemmas about eq_nat_dec	Jason Gross	2016-07-18
*	Fix some typos in the previous commit	Jason Gross	2016-07-18
*	Add some lemmas about nth_default in bounds	Jason Gross	2016-07-18
*	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
*	ported IterAssocOp to use monoid rather than a billion context variables that...	jadep	2016-07-18
*	Added lemmas to ZUtil and NatUtil (for Testbit)	jadep	2016-07-18
*	tuple: applying functions to tuples of arbitrary length	Andres Erbsen	2016-07-12
*	Merge of fixedlength and master	jadep	2016-07-11
\|\
\| *	wrap nsatz in Algebra	Andres Erbsen	2016-07-11
\| *	[congruence] is more powerful in 8.5 than in 8.4	Andres Erbsen	2016-07-11
\| *	merge	jadep	2016-07-10
\| \|\
\| * \|	added proofs about addition chain exponentiation for later use in ModularBase...	jadep	2016-07-10
\| \| *	Fix ListUtil for Coq 8.4	Jason Gross	2016-07-10
\| \| *	Update ListUtil	Jason Gross	2016-07-08
\| \| *	Fix NatUtil for 8.4	Jason Gross	2016-07-08
\| \| *	Add useful tactics and util lemmas	Jason Gross	2016-07-08
\| \| *	Add a NatUtil lemma and db	Jason Gross	2016-07-08
\| \| *	Add a ListUtil lemma	Jason Gross	2016-07-08
\| \| *	Add a ListUtil lemma	Jason Gross	2016-07-08
\| \| *	Add Z.div_0_l to ZUtil	Jason Gross	2016-07-08
\| \| *	Fix ListUtil for Coq 8.4	Jason Gross	2016-07-08
* \| \|	Util/Tuple: added a version of from_list that doesn't require a proof of leng...	jadep	2016-07-08
\| * \|	Util/Tuple: added a version of from_list that doesn't require a proof of leng...	jadep	2016-07-08
\| * \|	Added mod case to zero_bounds	jadep	2016-07-08
\| \| *	Add update_nth out of bounds	Jason Gross	2016-07-07
\| \| *	Add hint db in ListUtil	Jason Gross	2016-07-07
\| \| *	More ListUtil facts	Jason Gross	2016-07-07
\| \| *	Slightly better arguments in ListUtil	Jason Gross	2016-07-07
\| \| *	Correct hintdb names	Jason Gross	2016-07-07
\| \| *	Add more about firstn to listutil	Jason Gross	2016-07-07
\| \| *	Add more update_nth to ListUtil	Jason Gross	2016-07-07
\| \| *	Fix ListUtil for Coq 8.4	Jason Gross	2016-07-07
\| \| *	Add pow2_mod to ZUtil	Jason Gross	2016-07-07
\| \|/
\| *	Fix notations, add &	Jason Gross	2016-07-06
\| *	Add [update_nth] to ListUtil, change [set_nth]	Jason Gross	2016-07-06
\| *	Add notations for Z.shift{r,l} to ZUtil	Jason Gross	2016-07-06
\| *	Improve some reserved notations	Jason Gross	2016-07-06
\| *	Fix for broken 8.5 build in ListUtil	Jason Gross	2016-07-06
\| *	fixed indentation for new lemmas in ZUtil	jadep	2016-07-06