fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix a missing argument	Jason Gross	2017-02-03
\|
*	Fix a typo	Jason Gross	2017-02-03
\|
*	Handle more kinds of ops in fixed_size_op_to_word	Jason Gross	2017-02-03
\|
*	Only unfold the non-zpecialized versions of wcmovl, wcmovne, wneg	Jason Gross	2017-02-03
\| \| \| \|	The specialized versions don't match with the generic version; they'll need special behavior
*	Also unfold wcmovl, wcmovne, wneg in fixed_size_constants	Jason Gross	2017-02-03
\|
*	Don't autounfold wordToZ nor ZToWord	Jason Gross	2017-02-03
\| \| \| \|	The tactic fixed_size_op_to_word relies on them being folded.
*	Add fixed_size_op_to_word tactic	Jason Gross	2017-02-03
\|
*	Add interp_flat_type_rel_pointwise2_hetero_iff	Jason Gross	2017-02-03
\|
*	Add lemmas for Z ops Proper	Jason Gross	2017-02-03
\|
*	Add log2_up_le_full	Jason Gross	2017-02-03
\|
*	Add Z.log2_up_nonneg to zarith	Jason Gross	2017-02-03
\|
*	Reorder Reflection.Z.Syntax	Jason Gross	2017-02-02
\| \| \| \|	This puts all the definitions first, and then puts the interpretations after that
*	Split up Reflection/Z/Syntax and make it smaller	Jason Gross	2017-02-02
\|
*	Add wf database	Jason Gross	2017-02-01
\|
*	Generalize InlineInterp	Jason Gross	2017-02-01
\|
*	Fix lazymatch ordering	Jason Gross	2017-02-01
\|
*	More powerful preinvert_one_type	Jason Gross	2017-02-01
\| \| \| \|	It's be nice if we could find a uniform way to do this for all flat_types which resolve to constructors...
*	Add wordToZ_ZToWord_wordToZ	Jason Gross	2017-02-01
\|
*	Add ZToWord_wordToZ_ZToWord	Jason Gross	2017-02-01
\|
*	Add NToWord_wordToN_NToWord	Jason Gross	2017-02-01
\|
*	Add wordToZ_ZToWord, ZToWord_wordToZ	Jason Gross	2017-02-01
\|
*	Add invert_match_op	Jason Gross	2017-02-01
\|
*	Add invert_op	Jason Gross	2017-02-01
\|
*	Add inversion_expr	Jason Gross	2017-02-01
\|
*	Add invert_match_expr	Jason Gross	2017-02-01
\|
*	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
\|