From 21198245dab432d3c0ba2bb8a02254e7d0594382 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 6 Apr 2017 20:59:55 -0400 Subject: remove unused files --- _CoqProject | 6 ------ 1 file changed, 6 deletions(-) (limited to '_CoqProject') 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 -- cgit v1.2.3