fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Adapt to Coq's PR#8555	Maxime Dénès	2018-10-02
\|
*	Curves/Edwards/Affine: prove point compression admits	Andres Erbsen	2017-07-06
\|
*	Edwards coordinates precomputed addition formula	Andres Erbsen	2017-06-15
\|
*	ScalarMult: Z -> G -> G (closes #193)	Andres Erbsen	2017-06-14
\|
*	Don't rely on autogenerated names	Jason Gross	2017-06-05
\| \| \| \| \| \|	This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
*	Strip trailing whitespace	Jason Gross	2017-06-02
\| \| \| \| \| \| \|	With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ```
*	Prove relationship between `xzladderstep` and M.add (#162)	Andres Erbsen	2017-04-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	* hopefully all proofs we need about xzladderstep * Better automation in xzproofs * Speed up xzproofs with heuristic clearing * Remove useless hypotheses * XZProofs cleanup * fix "group by isomorphism" proofs, use in XZProofs
*	rename-everything	Andres Erbsen	2017-04-06