diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-12 14:44:48 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:39:03 -0400 |
| commit | 4c346d17e03f88a7ac5eb98cf2143563bae53bf4 (patch) | |
| tree | 1d62e2ae03683efde8e50203ca21e0104410f6f9 /_CoqProject | |
| parent | 6439b8ac778819ae4e3f0598bb38c8a256f7a9df (diff) | |
port some edwards curve theorems
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/_CoqProject b/_CoqProject index c1e10953f..02a3c797d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,5 +1,6 @@ -R src Crypto -src/CompleteEwardsCurve/Pre.v +src/CompleteEdwardsCurve/Pre.v +src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/Curves/PointFormats.v src/Curves/ScalarMult.v src/Galois/BaseSystem.v @@ -17,7 +18,7 @@ src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/Tutorial.v src/Rep/ECRep.v src/Rep/GaloisRep.v -src/Spec/CompleteEwardsCurve.v +src/Spec/CompleteEdwardsCurve.v src/Spec/ModularArithmetic.v src/Specific/EdDSA25519.v src/Specific/GF25519.v |