fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-04-19
\|\
\| *	Add a tactic for field inequalities	Jason Gross	2016-04-19
* \|	Cleaned up and revised DoubleAndAdd.	jadep	2016-04-15
* \|	Removed old iter_op version and its last dependency.	jadep	2016-04-15
\|/
*	Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...	jadep	2016-04-14
*	extended coordinates setoid boilerplate	Andres Erbsen	2016-03-20
*	Finish absolutizing imports	Jason Gross	2016-03-10
*	Remove [Admitted]; [Qed] is now under a second	Jason Gross	2016-03-08
*	CompleteEdwardsCurveTheorems: associativity proof that times out on Qed	Andres Erbsen	2016-03-03
*	ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoo...	Andres Erbsen	2016-02-28
*	moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ...	Jade Philipoom	2016-02-16
*	cleaned up and ported definition to solve for x ^ 2 in the curve equation	Jade Philipoom	2016-02-16
*	remove Check	Andres Erbsen	2016-02-15
*	Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into spec	Jade Philipoom	2016-02-15
\|\
* \|	ported some of EdDSA25519 to new field framework	Jade Philipoom	2016-02-15
\| *	port bounded iter_op and Edwards doubleAndAdd	Andres Erbsen	2016-02-15
\| *	CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context	Andres Erbsen	2016-02-15
\|/
*	EdDSA spec ported over to new field implementation	Jade Philipoom	2016-02-13
*	workaround field with typeclass modulus	Andres Erbsen	2016-02-12
*	fix imports	Andres Erbsen	2016-02-12
*	document field issue re-appearing	Andres Erbsen	2016-02-12
*	port some edwards curve theorems	Andres Erbsen	2016-02-12