aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Robert Sloan <varomodt@gmail.com>2016-06-23 19:31:11 -0400
committerGravatar Robert Sloan <varomodt@gmail.com>2016-06-23 19:31:11 -0400
commit14f41f622196bafcd9ad40543f21b72d88e01e7d (patch)
tree03e4259bc6a0411709e1ce3b34ce4624f1745799 /_CoqProject
parentcdd7cc8d0c51186558f90eee8fd7e19bebcdfda1 (diff)
Remove vestigal BoundedWord machinery
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject3
1 files changed, 0 insertions, 3 deletions
diff --git a/_CoqProject b/_CoqProject
index b1e422ae3..04e2c2f22 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,10 +8,8 @@ src/BaseSystemProofs.v
src/Testbit.v
src/Assembly/AlmostConversion.v
src/Assembly/AlmostQhasm.v
-src/Assembly/BoundedWord.v
src/Assembly/Conversion.v
src/Assembly/Language.v
-src/Assembly/MultiBoundedWord.v
src/Assembly/Pipeline.v
src/Assembly/Pseudize.v
src/Assembly/Pseudo.v
@@ -33,7 +31,6 @@ src/Encoding/ModularWordEncodingTheorems.v
src/Experiments/DerivationsOptionRectLetInEncoding.v
src/Experiments/GenericFieldPow.v
src/Experiments/SpecEd25519.v
-src/Galois/GaloisField.v
src/ModularArithmetic/ExtendedBaseVector.v
src/ModularArithmetic/ModularArithmeticTheorems.v
src/ModularArithmetic/ModularBaseSystem.v