aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Relations.v
Commit message (Collapse)AuthorAge
* Don't rely on autogenerated namesGravatar Jason Gross2017-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 whitespaceGravatar Jason Gross2017-06-02
| | | | | | | With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ```
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
|
* Add fieldwise_eq_edwards_extended_add_coordinates_carry_nocarryGravatar Jason Gross2016-11-17
|
* prove Proper_SRepERepMulGravatar Andres Erbsen2016-10-29
|
* alternative signing derivationGravatar Andres Erbsen2016-09-22
| | | | cleanup
* Derive EdDSA.verify from equational specificationGravatar Andres Erbsen2016-09-16
Experiments/SpecEd25519 will come back soon