aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2016-02-15 15:21:29 -0500
committerGravatar Robert Sloan <varomodt@gmail.com>2016-06-22 13:40:27 -0400
commit1a07a4a34a05b9a9dcabdd69c06e1618e76e80de (patch)
tree5c30c2ba92b2b868af191185893f5956c331a45f /_CoqProject
parent8ea3b32a5275b0c440afded57bfeb770b52f1e35 (diff)
Finish seperating our specs: remove old non-specified code
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject19
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