fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	put EdDSA encoding sign bit at the MSB	Andres Erbsen	2016-11-04
\|
*	Fix some subtleties with equalities in point encodings	jadep	2016-10-30
\|
*	Modify point_phi (from PointEncodings) to use ref_phi	jadep	2016-10-23
\|
*	Don't let [tauto] destruct [Equivalence] in PE	Jason Gross	2016-10-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This makes progress towards #75 (now src/Experiments/Ed25519.v builds with both 8.4 and 8.5). Quoting [the changelog](https://github.com/coq/coq/blob/trunk/CHANGES#L576): > - Tactic "tauto" was exceptionally able to destruct other connectives than the binary connectives "and", "or", "prod", "sum", "iff". This non-uniform behavior has been fixed (bug #2680) and tauto is slightly weaker (possible source of incompatibilities). On the opposite side, new tactic "dtauto" is able to destruct any record-like inductive types, superseding the old version of "tauto". There was an `Equivalence` in the context that `tauto` was destructing, but otherwise not using. This made the proof pick up an extra dependency from the context in 8.4, but not 8.5/8.6.
*	refactor scalar multiplication thoery, implement SRepERepMul	Andres Erbsen	2016-10-12
\|
*	Moved PointEncoding out of Spec	jadep	2016-10-06