aboutsummaryrefslogtreecommitdiff
path: root/src/Primitives/EdDSARepChange.v
Commit message (Collapse)AuthorAge
* Remove EdDSAGravatar Benjamin Barenblat2019-04-26
| | | | | Remove Spec/EdDSA.v and its reverse dependencies Spec/Ed25519.v and Primitives/EdDSARepChange.v. This code is no longer in use.
* Add Option.{lift,map,combine}, List.Option.liftGravatar Jason Gross2019-02-11
| | | | These will be useful for extending the AST with `option` types.
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
| | | | removing lemma wordToNat_wzero is ok because it's already in bbv
* typofixGravatar Andres Erbsen2017-06-14
|
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
|
* 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).
* rename-everythingGravatar Andres Erbsen2017-04-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 11:26:19 +0000