fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Handle renaming of NPeano.pow to Nat.pow (#3)	Jason Gross	2016-06-22
*	EdDSA.v: resolve ambiguity based on ed25519.py	Andres Erbsen	2016-06-21
*	Whitespace change	Jason Gross	2016-06-21
*	Fix a missing mod resolution	Jason Gross	2016-06-21
*	NPeano.modulo became Nat.modulo in 8.5	Jason Gross	2016-06-21
*	Import omega for 8.5	Jason Gross	2016-06-21
*	Shadowing of ltac constr-bound variables with identifiers is forbidden in 8.5	Jason Gross	2016-06-21
*	Use Admitted, not Qed, when a proof has admit	Jason Gross	2016-06-21
*	Fix [Proper_add] in 8.5	Jason Gross	2016-06-21
*	Make [bash] tactic easier to debug	Jason Gross	2016-06-21
*	use Local Obligation Tactic (8.5-compat)	Andres Erbsen	2016-06-21
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
*	Algebra: change a aliasing definition into an aliasing lemma to appease impli...	Andres Erbsen	2016-06-20
*	parenthesize Ltac [constr:] arguments	Andres Erbsen	2016-06-20
*	Fix nsatz_compute for 8.4	Jason Gross	2016-06-20
*	More missing scopes for 8.5?	Jason Gross	2016-06-20
*	More 8.5 fixes	Jason Gross	2016-06-20
*	Variosu 8.5 fixes	Jason Gross	2016-06-20
*	Fix for Coq 8.4pl2	Jason Gross	2016-06-20
*	move nsatz into tactics directory	Andres Erbsen	2016-06-20
*	remove obsolete rep mechanism	Andres Erbsen	2016-06-20
*	GF25519: quiet	Andres Erbsen	2016-06-20
*	Remove anything incompatible with new algebraic hierarcy	Andres Erbsen	2016-06-20
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\
\| *	[F q] is [Algebra.field]	Andres Erbsen	2016-06-20
\| *	port EdDSA spec	Andres Erbsen	2016-06-20
\| *	tuple tooling	Andres Erbsen	2016-06-20
\| *	port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...	Andres Erbsen	2016-06-18
* \|	Canonicalization is now automated in GF25519 and added to GF1305.	jadep	2016-06-17
* \|	Specific version of freeze for GF25519 (automation still needs a little work)	jadep	2016-06-17
\| *	move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems	Andres Erbsen	2016-06-17
\| *	Z is integral domain	Andres Erbsen	2016-06-16
\| *	port edwards curve spec	Andres Erbsen	2016-06-16
\| *	edwards curve addition respects field homomorphism	Andres Erbsen	2016-06-16
\| *	algebra: add homomorphisms	Andres Erbsen	2016-06-16
\| *	prove ring admits	Andres Erbsen	2016-06-16
\| *	edwards curve preliminaries: replace oncurve proof with nsatz	Andres Erbsen	2016-06-16
\| *	nsatz: reimplement, integrate, demonstrate	Andres Erbsen	2016-06-15
* \|	PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...	jadep	2016-06-15
* \|	changed representation definition to require digits vector to be the exact le...	jadep	2016-06-15
* \|	Added canonicalization to ModularBaseSystemOpt.	jadep	2016-06-15
* \|	Merge	jadep	2016-06-14
\|\ \
* \| \|	Finished admits for canonicalization proofs.	jadep	2016-06-14
\| \| *	refactor nsatz wrappers into algebra file	Andres Erbsen	2016-06-14
\| \| *	[field] and [nsatz] do things now again	Andres Erbsen	2016-06-14
* \| \|	reversed modulus_digits and proved a few admits	jadep	2016-06-13
* \| \|	progress on second stage (conditional constant-time subtraction) of canonical...	jadep	2016-06-13
\| \| *	stuck because overloading-by-typeclasses sucks	Andres Erbsen	2016-06-13
\| \| *	indent	Andres Erbsen	2016-06-12
\| * \|	Another fix for an anomaly in 8.4pl2	Jason Gross	2016-06-11