fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Redo MultiSizeTest with generic framework	Jason Gross	2017-01-01
\|
*	Transparent versions of {flat_,}type_eq_dec	Jason Gross	2017-01-01
\|
*	Add generic code for MultiSizeTest	Jason Gross	2017-01-01
\|
*	Add smart_interp_map_gen	Jason Gross	2017-01-01
\|
*	Add SmartFlatTypeMap2	Jason Gross	2016-12-26
\|
*	Add flatten_flat_type	Jason Gross	2016-12-26
\|
*	Fix Coq 8.6 warnings	Jason Gross	2016-12-26
\|
*	MultiSizeTest: a basic example of the scheme I have in mind for bounds ↵	Adam Chlipala	2016-12-25
\| \| \| \|	inference with multiple candidate word sizes
*	Fix 8.4 build issues	Jason Gross	2016-12-15
\|
*	Fix 8.4 issues	Jason Gross	2016-12-15
\|
*	Work around bug in 8.4 implicits	Jason Gross	2016-12-14
\|
*	Work around bug in 8.4 apply	Jason Gross	2016-12-14
\|
*	Admit Common9_4Op.v	Jason Gross	2016-12-08
\|
*	Don't use UIP in inversion_wff	Jason Gross	2016-12-03
\|
*	Add inversion_wff	Jason Gross	2016-12-03
\|
*	Add WfInversion	Jason Gross	2016-12-03
\|
*	More powerful inversion_option	Jason Gross	2016-12-03
\|
*	Move things to ExprInversion	Jason Gross	2016-12-03
\|
*	Add invert_Var	Jason Gross	2016-12-03
\|
*	Arguments for invert_Op	Jason Gross	2016-12-03
\|
*	Fewer autogenerated names	Jason Gross	2016-12-03
\|
*	Add invert_Op	Jason Gross	2016-12-03
\|
*	Change some default names	Jason Gross	2016-12-03
\|
*	copy_bounds.sh	Jason Gross	2016-12-02
\|
*	Fix looping in Coq 8.4 in ExtendedAddCoordinates.v	Jason Gross	2016-12-02
\|
*	Initial (not fully working) version of MapWithInterpInfo	Jason Gross	2016-12-02
\|
*	Add SmartFlatTypeMapUnInterp	Jason Gross	2016-12-02
\|
*	Add invert_LetIn	Jason Gross	2016-12-02
\|
*	Arguments for invert_Pair	Jason Gross	2016-12-02
\|
*	Add invert_Pair	Jason Gross	2016-12-02
\|
*	Add SmartFlatTypeMapInterp	Jason Gross	2016-12-02
\|
*	SmartFlatTypeMap arguments	Jason Gross	2016-12-02
\|
*	Add SmartFlatTypeMap	Jason Gross	2016-12-02
\|
*	Minor change to inm_op_correct_and_bounded_prefix	Jason Gross	2016-11-25
\|
*	Fix a typo	Jason Gross	2016-11-25
\|
*	Add inm_op_correct_and_bounded_iff_prefix	Jason Gross	2016-11-25
\|
*	Add inm_op_correct_and_bounded	Jason Gross	2016-11-25
\|
*	Also git add in copy_bounds	Jason Gross	2016-11-25
\|
*	uncurry_n_op_fe25519	Jason Gross	2016-11-25
\|
*	Various application lemmas	Jason Gross	2016-11-23
\|
*	More GF25519ReflectiveCommon generalization	Jason Gross	2016-11-22
\|
*	Add tuple lemmas	Jason Gross	2016-11-22
\|
*	Add lemmas about application	Jason Gross	2016-11-22
\|
*	Add impl_under_tower	Jason Gross	2016-11-22
\|
*	Add hlistP	Jason Gross	2016-11-22
\|
*	Add rhlist	Jason Gross	2016-11-22
\|
*	Add interp_all_binders_for'	Jason Gross	2016-11-22
\|
*	Add tower_nd	Jason Gross	2016-11-22
\|
*	Fix for 8.6	Jason Gross	2016-11-22
\|
*	Copy bounds, fix a typo	Jason Gross	2016-11-22
\|