diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-13 22:09:21 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:39:04 -0400 |
| commit | 75926e67a551d99153bccf8fe82c8eabc0b9ebcd (patch) | |
| tree | fda18a059a2e774b74146496104092114e2a6030 /_CoqProject | |
| parent | bca928f049b75c13fd3c376c287c568020935534 (diff) | |
Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject index 02a3c797d..e6991793b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,8 +1,9 @@ -R src Crypto -src/CompleteEdwardsCurve/Pre.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +src/CompleteEdwardsCurve/Pre.v src/Curves/PointFormats.v src/Curves/ScalarMult.v +src/EdDSAProofs.v src/Galois/BaseSystem.v src/Galois/EdDSA.v src/Galois/Galois.v @@ -19,6 +20,7 @@ src/ModularArithmetic/Tutorial.v src/Rep/ECRep.v src/Rep/GaloisRep.v src/Spec/CompleteEdwardsCurve.v +src/Spec/EdDSA.v src/Spec/ModularArithmetic.v src/Specific/EdDSA25519.v src/Specific/GF25519.v |