fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Lemmas about winit, wlast	Rob Sloan	2016-11-11
*	prove last HList admit	Andres Erbsen	2016-11-11
*	prove admits in Util.Tuple	Andres Erbsen	2016-11-11
*	[cbn] is 8.5 only	Jason Gross	2016-11-11
*	Fix for Coq 8.4	Jason Gross	2016-11-11
*	Fix proofs broken by stronger preconditions	Jason Gross	2016-11-11
*	Most of the admits in Ed25519.v	Rob Sloan	2016-11-11
*	extraction less slow	Andres Erbsen	2016-11-11
*	Add Tuple and HList lemmas	Jason Gross	2016-11-10
*	Work around looping in 8.4	Jason Gross	2016-11-10
*	More proof fixes	Jason Gross	2016-11-10
*	Fix for 8.4	Jason Gross	2016-11-10
*	Minimize diff with master, fix some proofs that were broken	Jason Gross	2016-11-10
*	Hint Rewrite is section-local; move to top-level	Jason Gross	2016-11-10
*	Remove WordizeUtil dependency from WordUtil	Rob Sloan	2016-11-09
*	Merge with master	Rob Sloan	2016-11-09
\|\
\| *	Fix for 8.4	Jason Gross	2016-11-09
\| *	Switch to accurate bounds for lor	Jason Gross	2016-11-09
* \|	Rebase + remove WordizeUtil dependency from Z/Interpretations	Rob Sloan	2016-11-09
\|\ \
\| \| *	Remove last admitted lemma in src/Reflection/Z/Interpretations/Relations.v	Jason Gross	2016-11-09
\| \|/
\| *	Fix bug in 8.4 build	Jason Gross	2016-11-09
\| *	Rewrite cast_word so that it's extracted better	Jason Gross	2016-11-09
\| *	Silence a warning about name collision	Jason Gross	2016-11-09
\| *	Fix bug in 8.4	Jason Gross	2016-11-09
\| *	Split up GF25519Reflective.Common: faster+parallel	Jason Gross	2016-11-09
* \|	Finished WordUtil, word operations in Z/Interpretation	Rob Sloan	2016-11-09
\| *	Add assoc_right	Jason Gross	2016-11-09
\| *	Fix Tuple.map2_S	Jason Gross	2016-11-09
* \|	Not quite done with WordUtil lemmas.	Robert Sloan	2016-11-08
\|\ \
\| \| *	Add Tuple.map2_S	Jason Gross	2016-11-08
\| \| *	Fix for Coq 8.4	Jason Gross	2016-11-08
\| \| *	Fix f_equiv brokenness in 8.4, even faster src/MxDHRepChange.v	Jason Gross	2016-11-08
\| \| *	Faster build of src/MxDHRepChange.v	Jason Gross	2016-11-08
\| \| *	Some fixes for 8.4 differences	Jason Gross	2016-11-08
\| \| *	More progress on src/Reflection/Z/Interpretations/Relations.v	Jason Gross	2016-11-08
\| \| *	Fix precedence issue with 8.4	Jason Gross	2016-11-08
\| \| *	Add map2_map{,_fst,_snd}	Jason Gross	2016-11-08
\| \| *	Add hlist_map	Jason Gross	2016-11-08
\| \| *	Fix 8.4 build ([value] is a constant)	Jason Gross	2016-11-08
\| \| *	Prove things in ModularBaseSystemListZOperationsProofs	Jason Gross	2016-11-08
\| \|/
\| *	Factor related_Z_op (except conditional_sub)	Jason Gross	2016-11-08
\| *	More factoring in related_Z_op	Jason Gross	2016-11-08
\| *	Fix some qualified name issues with previous commit	Jason Gross	2016-11-08
\| *	Add word64ToZ_{neg,cmovne,cmovle,conditional_subtract}	Jason Gross	2016-11-08
\| *	Add HList.const	Jason Gross	2016-11-08
\| *	Rename iffT, add some lemmas about tuple and hlist	Jason Gross	2016-11-08
\| *	Add log2_lt_pow2_alt	Jason Gross	2016-11-08
\| *	Remove lor admit in relations	Jason Gross	2016-11-08
\| *	Work around bug in 8.4	Jason Gross	2016-11-08
\| *	Work around bug 5189 (broken [Hint Resolve ->])	Jason Gross	2016-11-08