1 files changed, 5 insertions, 4 deletions
diff --git a/_CoqProject b/_CoqProject
index 3f2d895f5..afeab0c02 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -228,6 +228,7 @@ src/Spec/MontgomeryCurve.v
 src/Spec/MxDH.v
 src/Spec/WeierstrassCurve.v
 src/Spec/Test/X25519.v
+src/Specific/ArithmeticSynthesisFramework.v
 src/Specific/ArithmeticSynthesisTest130.v
 src/Specific/CurveParameters.v
 src/Specific/IntegrationTestDisplayCommon.v
@@ -252,8 +253,10 @@ src/Specific/IntegrationTestSub.v
 src/Specific/IntegrationTestSubDisplay.v
 src/Specific/IntegrationTestTemporaryMiscCommon.v
 src/Specific/Karatsuba.v
+src/Specific/LadderstepSynthesisFramework.v
 src/Specific/MontgomeryP256_128.v
 src/Specific/ReificationTypes.v
+src/Specific/SynthesisFramework.v
 src/Specific/NISTP256/AMD64/MontgomeryP256.v
 src/Specific/NISTP256/AMD64/feadd.v
 src/Specific/NISTP256/AMD64/feaddDisplay.v
@@ -268,16 +271,14 @@ src/Specific/NISTP256/AMD64/fesubDisplay.v
 src/Specific/NISTP256/FancyMachine256/Barrett.v
 src/Specific/NISTP256/FancyMachine256/Core.v
 src/Specific/NISTP256/FancyMachine256/Montgomery.v
-src/Specific/X25519/C32/ArithmeticSynthesisTest.v
 src/Specific/X25519/C32/CurveParameters.v
-src/Specific/X25519/C32/ReificationTypes.v
+src/Specific/X25519/C32/Synthesis.v
 src/Specific/X25519/C32/femul.v
 src/Specific/X25519/C32/femulDisplay.v
 src/Specific/X25519/C32/fesquare.v
 src/Specific/X25519/C32/fesquareDisplay.v
-src/Specific/X25519/C64/ArithmeticSynthesisTest.v
 src/Specific/X25519/C64/CurveParameters.v
-src/Specific/X25519/C64/ReificationTypes.v
+src/Specific/X25519/C64/Synthesis.v
 src/Specific/X25519/C64/femul.v
 src/Specific/X25519/C64/femulDisplay.v
 src/Specific/X25519/C64/fesquare.v