diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-15 15:21:29 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:40:27 -0400 |
| commit | 1a07a4a34a05b9a9dcabdd69c06e1618e76e80de (patch) | |
| tree | 5c30c2ba92b2b868af191185893f5956c331a45f /_CoqProject | |
| parent | 8ea3b32a5275b0c440afded57bfeb770b52f1e35 (diff) | |
Finish seperating our specs: remove old non-specified code
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 19 |
1 files changed, 3 insertions, 16 deletions
diff --git a/_CoqProject b/_CoqProject index 0b8aaa6bf..86cb1ae98 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,33 +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/Encoding.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 |