fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add SmartVarfMap3 arguments	Jason Gross	2017-03-28
\|
*	Add SmartVarfMap3	Jason Gross	2017-03-28
\|
*	Fix more unfolding	Jason Gross	2017-03-10
\|
*	Make sure interp_flat_type isn't unfolded in SmartMap	Jason Gross	2017-03-10
\|
*	Add better SmartFlatTypeMapInterp2	Jason Gross	2017-03-08
\|
*	make 8.5 happy	Andres Erbsen	2017-03-02
\|
*	Switch to fully uncurried form for reflection	Jason Gross	2017-03-01
\| \| \| \| \| \| \| \| \| \| \|	This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes.
*	Add SmartVarfMap Proper instance	Jason Gross	2017-02-28
\|
*	Add various reflection improvements, boundbycast	Jason Gross	2017-02-21
\|
*	Remove the let-in from SmartValf	Jason Gross	2017-02-07
\| \| \| \|	It messes with reduction elsewhere
*	Fix implicits	Jason Gross	2017-01-31
\|
*	Add SmartFlatTypeMap2Interp2	Jason Gross	2017-01-31
\|
*	Add In_G_wff_SmartVarf, SmartVarf_Pair	Jason Gross	2017-01-30
\|
*	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
\|
*	Split off some bits of Reflection.Syntax	Jason Gross	2017-01-26
	Also split off some bits of Util.Tactics