fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add invert_expr	Jason Gross	2017-02-01
\|
*	Add wff_SmartVarVarf_nil	Jason Gross	2017-02-01
\|
*	Bump submodule for better travis timing logs	Jason Gross	2017-01-31
\|
*	Preferentially invert wff with two constructors	Jason Gross	2017-01-31
\|
*	Absolutize some imports	Jason Gross	2017-01-31
\|
*	Absolutize some imports	Jason Gross	2017-01-31
\|
*	Nicer inversion_wff	Jason Gross	2017-01-31
\|
*	Split off unique {pose,assert}	Jason Gross	2017-01-31
\|
*	Fix implicits	Jason Gross	2017-01-31
\|
*	Add SmartFlatTypeMap2Interp2	Jason Gross	2017-01-31
\|
*	Don't change sumbool eq hypothesis unless both sides are constructors	Jason Gross	2017-01-30
\|
*	Fix typos	Jason Gross	2017-01-30
\|
*	Add Util.Sumbool	Jason Gross	2017-01-30
\|
*	Add inversion_flat_type, inversion_type	Jason Gross	2017-01-30
\|
*	Add In_G_wff_SmartVarf, SmartVarf_Pair	Jason Gross	2017-01-30
\|
*	Add interp_flat_type_rel_pointwise0	Jason Gross	2017-01-27
\|
*	Better typing for SmartPairf_Pair	Jason Gross	2017-01-27
\| \| \| \|	Previously, interp_flat_type got unfolded, which interfered with setoid_rewrite
*	Remove dead code	Jason Gross	2017-01-27
\|
*	Add SmartPairf_Pair	Jason Gross	2017-01-27
\|
*	Doc fixup	Jason Gross	2017-01-27
\|
*	Various minor reflection fixups	Jason Gross	2017-01-27
\|
*	Split off some bits of Reflection.Syntax	Jason Gross	2017-01-26
\| \| \| \|	Also split off some bits of Util.Tactics
*	Add interp_type_rel_pointwise2_hetero	Jason Gross	2017-01-25
\|
*	Add interp_flat_type_rel_pointwise2_hetero_flatten_binding_list2	Jason Gross	2017-01-25
\|
*	Add flatten_binding_list2_SmartVarfMap{1,2}	Jason Gross	2017-01-25
\|
*	Lemmas about flatten_binding_list2	Jason Gross	2017-01-25
\|
*	Add flatten_binding_list2	Jason Gross	2017-01-25
\|
*	Add interp_flat_type_rel_pointwise2_hetero	Jason Gross	2017-01-25
\|
*	Generalize flatten_binding_list_SmartValf	Jason Gross	2017-01-24
\|
*	Add flatten_binding_list_SmartValf	Jason Gross	2017-01-24
\|
*	Add SmartFlatTypeUnMap	Jason Gross	2017-01-24
\|
*	Add flatten_binding_list_SmartVarfMap	Jason Gross	2017-01-24
\|
*	Add SmartVarf{Type,Prop}Map{,2}	Jason Gross	2017-01-24
\|
*	Add SmartVarfMap_id	Jason Gross	2017-01-24
\|
*	Add SmartVarfMap2	Jason Gross	2017-01-24
\|
*	Add smart_interp_flat_map2	Jason Gross	2017-01-24
\|
*	Add match commutation lemmas	Jason Gross	2017-01-23
\|
*	Preserve names in invert_expr_subst	Jason Gross	2017-01-23
\|
*	Make invert_expr_subst not loop	Jason Gross	2017-01-23
\|
*	Fix invert_expr_subst	Jason Gross	2017-01-23
\|
*	Better invert_expr	Jason Gross	2017-01-23
\|
*	Minor additions	Jason Gross	2017-01-23
\|
*	Fix a typo	Jason Gross	2017-01-23
\|
*	Add invert_expr_subst	Jason Gross	2017-01-23
\|
*	Allow inversion on wff if either side is not a var	Jason Gross	2017-01-23
\|
*	Don't remake .v.d. files in clean-coqprime	Jason Gross	2017-01-22
\|
*	Update _CoqProject	Jason Gross	2017-01-21
\|
*	Add transparent equality proofs for fixed wordT	Jason Gross	2017-01-21
\| \| \| \|	Such a pain to make proofs compute
*	Revert "Fix a missing qualification"	Jason Gross	2017-01-21
\| \| \| \| \| \| \| \| \| \|	This reverts commit 3c4ff8fe8d2154addcf440690d315c58a529c1f6. Revert "Move weqb_hetero to Bedrock.Word" This reverts commit c83cb07f1477de33ce9eb43eea6a4f2720a94763. We probably shouldn't modify Bedrock.Word
*	Fix a missing qualification	Jason Gross	2017-01-21
\|