merging with master

1 files changed, 16 insertions, 1 deletions

diff --git a/_CoqProject b/_CoqProject
index d4a8857a1..bb92c783a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,26 +1,40 @@
 -R src Crypto
 src/BaseSystem.v
-src/BoundedIterOp.v
+src/BaseSystemProofs.v
 src/EdDSAProofs.v
+src/Rep.v
+src/Testbit.v
 src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
 src/CompleteEdwardsCurve/DoubleAndAdd.v
 src/CompleteEdwardsCurve/ExtendedCoordinates.v
 src/CompleteEdwardsCurve/Pre.v
 src/Encoding/EncodingTheorems.v
+src/Encoding/ModularWordEncodingPre.v
+src/Encoding/ModularWordEncodingTheorems.v
+src/Encoding/PointEncodingPre.v
+src/Encoding/PointEncodingTheorems.v
+src/ModularArithmetic/ExtendedBaseVector.v
 src/ModularArithmetic/FField.v
 src/ModularArithmetic/FNsatz.v
 src/ModularArithmetic/ModularArithmeticTheorems.v
 src/ModularArithmetic/ModularBaseSystem.v
+src/ModularArithmetic/ModularBaseSystemOpt.v
+src/ModularArithmetic/ModularBaseSystemProofs.v
 src/ModularArithmetic/Pre.v
 src/ModularArithmetic/PrimeFieldTheorems.v
+src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+src/ModularArithmetic/PseudoMersenneBaseParams.v
+src/ModularArithmetic/PseudoMersenneBaseRep.v
 src/ModularArithmetic/Tutorial.v
 src/Spec/CompleteEdwardsCurve.v
 src/Spec/Ed25519.v
 src/Spec/EdDSA.v
 src/Spec/Encoding.v
 src/Spec/ModularArithmetic.v
+src/Spec/ModularWordEncoding.v
 src/Spec/PointEncoding.v
 src/Specific/Ed25519.v
+src/Specific/GF1305.v
 src/Specific/GF25519.v
 src/Tactics/VerdiTactics.v
 src/Util/CaseUtil.v
@@ -28,6 +42,7 @@ src/Util/IterAssocOp.v
 src/Util/ListUtil.v
 src/Util/NatUtil.v
 src/Util/NumTheoryUtil.v
+src/Util/Tactics.v
 src/Util/WordUtil.v
 src/Util/ZUtil.v
 src/Assembly/QhasmCommon.v