aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Option.v
Commit message (Collapse)AuthorAge
* added proofs about addition chain exponentiation for later use in ↵Gravatar jadep2016-07-10
| | | | ModularBaseSystem [pow], which we need for sqrt and inversion.
* EdDSA: prove things about specGravatar Andres Erbsen2016-06-25