fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Work around bug in 8.4 apply	Jason Gross	2016-12-14
\|
*	More powerful inversion_option	Jason Gross	2016-12-03
\|
*	Fix for Coq 8.5, 8.5pl1	Jason Gross	2016-10-18
\|
*	generalize equiv relations in Util.Option and EdDSARepChange	Andres Erbsen	2016-10-12
\|
*	Fix for Coq 8.5	Jason Gross	2016-09-16
\|
*	Derive EdDSA.verify from equational specification	Andres Erbsen	2016-09-16
\| \| \| \|	Experiments/SpecEd25519 will come back soon
*	Make [inversion_option] work on Prop options	Jason Gross	2016-09-03
\|
*	Rename congrunce_option to inversion_option, add [inversion_prod]	Jason Gross	2016-08-31
\|
*	Add congruence_option tactic	Jason Gross	2016-08-31
\|
*	added proofs about addition chain exponentiation for later use in ↵	jadep	2016-07-10
\| \| \| \|	ModularBaseSystem [pow], which we need for sqrt and inversion.
*	EdDSA: prove things about spec	Andres Erbsen	2016-06-25