diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-15 15:21:29 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-15 15:21:49 -0500 |
| commit | c711c52d057024c4b40a86f6f77f2e96ae2208ef (patch) | |
| tree | e032092b0313157fe0d3848370616855c30bd845 /_CoqProject | |
| parent | 0b5115da9d2b1d9a32bdb11eb9f81ceec9999c1d (diff) | |
Finish seperating our specs: remove old non-specified code
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 18 |
1 files changed, 3 insertions, 15 deletions
diff --git a/_CoqProject b/_CoqProject index fab90e35e..86cb1ae98 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,32 +1,20 @@ -R src Crypto +src/BaseSystem.v src/BoundedIterOp.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.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 -src/Galois/GaloisField.v -src/Galois/GaloisRep.v -src/Galois/GaloisTheory.v -src/Galois/GaloisTutorial.v -src/Galois/ModularBaseSystem.v -src/Galois/ModularBaseSystem.v src/ModularArithmetic/ModularArithmeticTheorems.v +src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/Tutorial.v -src/Rep/ECRep.v -src/Rep/GaloisRep.v src/Spec/CompleteEdwardsCurve.v src/Spec/EdDSA.v -src/Spec/EdDSA25519.v +src/Spec/Ed25519.v src/Spec/ModularArithmetic.v -src/Specific/EdDSA25519.v src/Specific/GF25519.v src/Tactics/VerdiTactics.v src/Util/CaseUtil.v |