fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Finished WordUtil, word operations in Z/Interpretation	Rob Sloan	2016-11-09
*	Not quite done with WordUtil lemmas.	Robert Sloan	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
\| *	Add Z.lor_nonneg to zarith	Jason Gross	2016-11-08
\| *	Minor refactoring of related_Z_op	Jason Gross	2016-11-07
\| *	Finish related_bounds_t_map1_tuple2	Jason Gross	2016-11-07
\| *	Add push_lift_option	Jason Gross	2016-11-07
\| *	More progress on related_bounds_t_map1_tuple2	Jason Gross	2016-11-07
\| *	More progress on t_map1_tuple2 lemmas	Jason Gross	2016-11-07
\| *	Add flat_interp_tuple_untuple'	Jason Gross	2016-11-07
\| *	Add flat_interp_untuple'_tuple	Jason Gross	2016-11-07
\| *	Add map_is_mapt'	Jason Gross	2016-11-07
\| *	Add IffT, some Proper prod lemmas	Jason Gross	2016-11-07
\| *	Add Proper prod instance	Jason Gross	2016-11-07
\| *	Add convoy_destruct	Jason Gross	2016-11-07
\| *	Add tuple hd and tl	Jason Gross	2016-11-07
\| *	Merge branch 'master' of ssh://github.com/mit-plv/fiat-crypto	Adam Chlipala	2016-11-07
\| \|\
\| * \|	Some progress on Relations admits	Adam Chlipala	2016-11-07
\| \| *	automate MxDHRepChange.Proper_loopiter intros	Andres Erbsen	2016-11-07
\| \|/
\| *	implement X25519	Andres Erbsen	2016-11-06
\| *	move B_order_l and prime_q	Andres Erbsen	2016-11-06
\| *	More reorg in Reflection/Z/Interpretations/Relations.v	Jason Gross	2016-11-06
\| *	Do some of the related_Z_op proofs	Jason Gross	2016-11-06
\| *	Refactor various reflective things	Jason Gross	2016-11-06
\| *	Add more admitted tuple lemmas	Jason Gross	2016-11-06
\| *	Add more admitted tuple lemmas	Jason Gross	2016-11-06
\| *	Add Tuple.map_map2 (admitted)	Jason Gross	2016-11-06
\| *	Add HList lemma	Jason Gross	2016-11-06
\| *	Add admitted lemma about tuple map, add hlist lem	Jason Gross	2016-11-06
\| *	Add Tuple lift push	Jason Gross	2016-11-06
\| *	Connect [is_bounded] to [bounded_by]	Jason Gross	2016-11-06
\| *	Fixes for Coq 8.4	Jason Gross	2016-11-06
\| *	The fix in 8.4 broke 8.5/8.6, so we fix that	Jason Gross	2016-11-06
\| *	Preliminary support: conditional sub as primitive	Jason Gross	2016-11-06
\| *	Add syntactic tuples	Jason Gross	2016-11-06
\| *	Add functions for [tuple (option _) _]	Jason Gross	2016-11-06
\| *	Add support for dependent reification	Jason Gross	2016-11-06
\| *	Work around broken evars in 8.4	Jason Gross	2016-11-06
\| *	More partial proofs	Jason Gross	2016-11-06
\| *	Prove inversion principles for bounded words	Jason Gross	2016-11-06
\| *	Plug in boundedness proofs	Jason Gross	2016-11-05