fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
*	Add interpf_LetIn	Jason Gross	2016-11-17
*	: assert is not valid 8.4 syntax	Jason Gross	2016-11-17
*	Add Un{Return,Abs}_eta	Jason Gross	2016-11-16
*	Add : assert to a bunch of arguments	Jason Gross	2016-11-16
*	Split fixedpoint in interpf	Jason Gross	2016-11-16
*	Arguments for Un{Return,Abs}	Jason Gross	2016-11-16
*	Add UnReturn, UnAbs	Jason Gross	2016-11-16
*	Support for 128-bit words	Jason Gross	2016-11-14
*	Add word-size-independent interpretations	Jason Gross	2016-11-14
*	Fix reification of neg	Jason Gross	2016-11-11
*	Make [neg] a unary operation in reflection	Jason Gross	2016-11-11
*	Remove more conditional subtract	Jason Gross	2016-11-11
*	Remove extra conditional subtract things	Jason Gross	2016-11-11
*	Remove special code for reified conditional sub	Jason Gross	2016-11-11
*	More proof fixes	Jason Gross	2016-11-10
*	Minimize diff with master, fix some proofs that were broken	Jason Gross	2016-11-10
*	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
\| \|/
* \|	Finished WordUtil, word operations in Z/Interpretation	Rob Sloan	2016-11-09
* \|	Not quite done with WordUtil lemmas.	Robert Sloan	2016-11-08
\|\ \
\| \| *	Fix for Coq 8.4	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 8.4 build ([value] is a constant)	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
\| *	Remove lor admit in relations	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
\| *	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
\| *	Some progress on Relations admits	Adam Chlipala	2016-11-07
\| *	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
\| *	Fixes for Coq 8.4	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 support for dependent reification	Jason Gross	2016-11-06
\| *	More partial proofs	Jason Gross	2016-11-06
\| *	Prove inversion principles for bounded words	Jason Gross	2016-11-06
\| *	Add related_word64_boundsi'	Jason Gross	2016-11-05
\| *	Split off some things from Interpretations	Jason Gross	2016-11-05