diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-04-06 20:59:55 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-04-06 20:59:55 -0400 |
| commit | 21198245dab432d3c0ba2bb8a02254e7d0594382 (patch) | |
| tree | 52d2fda30cd352d89c58c709d3367ca85423509a /_CoqProject | |
| parent | 18283278b4bd539a6d71d2dec26c8daa3a17230b (diff) | |
remove unused files
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/_CoqProject b/_CoqProject index d545cc6b2..823fda21b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -23,13 +23,10 @@ src/BoundedArithmetic/ArchitectureToZLike.v src/BoundedArithmetic/ArchitectureToZLikeProofs.v src/BoundedArithmetic/BaseSystem.v src/BoundedArithmetic/BaseSystemProofs.v -src/BoundedArithmetic/CaseUtil.v -src/BoundedArithmetic/Eta.v src/BoundedArithmetic/Interface.v src/BoundedArithmetic/InterfaceProofs.v src/BoundedArithmetic/Pow2Base.v src/BoundedArithmetic/Pow2BaseProofs.v -src/BoundedArithmetic/StripCF.v src/BoundedArithmetic/Double/Core.v src/BoundedArithmetic/Double/Proofs/BitwiseOr.v src/BoundedArithmetic/Double/Proofs/Decode.v @@ -46,8 +43,6 @@ src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/EdwardsMontgomery.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v -src/Experiments/ExtrHaskellNats.v -src/Experiments/GenericFieldPow.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v @@ -190,7 +185,6 @@ src/Spec/MxDH.v src/Spec/WeierstrassCurve.v src/Specific/IntegrationTest.v src/Specific/NewBaseSystemTest.v -src/Specific/SC25519.v src/Specific/FancyMachine256/Barrett.v src/Specific/FancyMachine256/Core.v src/Specific/FancyMachine256/Montgomery.v |