fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Update .mailmap	Jason Gross	2016-11-11
*	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
*	Merge pull request #91 from mit-plv/rsloan-patch-wordutil-admits	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