aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Robert Sloan <varomodt@gmail.com>2016-09-24 09:49:32 -0700
committerGravatar Robert Sloan <varomodt@gmail.com>2016-09-24 09:49:32 -0700
commit5050064f1fce8f3a8016ee424e075c203efcc2cc (patch)
tree999c34bf2684df48b1aec860bb8461ddd9f6c221 /_CoqProject
parent25ca3abcac4d9934d9511bc1a79223cd145e3a78 (diff)
Large-scale refactoring of src/Assembly
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject14
1 files changed, 5 insertions, 9 deletions
diff --git a/_CoqProject b/_CoqProject
index 5be286e95..f50b2a1d6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,17 +6,14 @@ src/Algebra.v
src/BaseSystem.v
src/BaseSystemProofs.v
src/Testbit.v
-src/Assembly/AlmostConversion.v
-src/Assembly/AlmostQhasm.v
src/Assembly/Bounds.v
-src/Assembly/Conversion.v
+src/Assembly/Compile.v
+src/Assembly/Conversions.v
src/Assembly/Evaluables.v
-src/Assembly/Language.v
-src/Assembly/Listize.v
+src/Assembly/HL.v
+src/Assembly/LL.v
+src/Assembly/PhoasCommon.v
src/Assembly/Pipeline.v
-src/Assembly/Pseudize.v
-src/Assembly/Pseudo.v
-src/Assembly/PseudoConversion.v
src/Assembly/Qhasm.v
src/Assembly/QhasmCommon.v
src/Assembly/QhasmEvalCommon.v
@@ -35,7 +32,6 @@ src/Experiments/DerivationsOptionRectLetInEncoding.v
src/Experiments/EdDSARefinement.v
src/Experiments/GenericFieldPow.v
src/Experiments/SpecEd25519.v
-src/Experiments/SpecificCurve25519.v
src/ModularArithmetic/ExtPow2BaseMulProofs.v
src/ModularArithmetic/ExtendedBaseVector.v
src/ModularArithmetic/ModularArithmeticTheorems.v