1 files changed, 18 insertions, 12 deletions
diff --git a/_CoqProject b/_CoqProject
index 5bcc76f6c..d36554986 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -228,22 +228,13 @@ src/Spec/MontgomeryCurve.v
 src/Spec/MxDH.v
 src/Spec/WeierstrassCurve.v
 src/Spec/Test/X25519.v
-src/Specific/IntegrationTestMontgomeryP256_128.v
-src/Specific/IntegrationTestMontgomeryP256_128Display.v
-src/Specific/IntegrationTestMontgomeryP256_128_Add.v
-src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v
-src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
-src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v
-src/Specific/IntegrationTestMontgomeryP256_128_Opp.v
-src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v
-src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
-src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v
-src/Specific/MontgomeryP256_128.v
 src/Specific/Framework/CurveParameters.v
 src/Specific/Framework/CurveParametersPackage.v
 src/Specific/Framework/IntegrationTestDisplayCommon.v
 src/Specific/Framework/IntegrationTestDisplayCommonTactics.v
 src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
+src/Specific/Framework/MontgomeryReificationTypes.v
+src/Specific/Framework/MontgomeryReificationTypesPackage.v
 src/Specific/Framework/Packages.v
 src/Specific/Framework/ReificationTypes.v
 src/Specific/Framework/ReificationTypesPackage.v
@@ -259,8 +250,23 @@ src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v
 src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
 src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v
 src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
+src/Specific/Framework/ArithmeticSynthesis/Montgomery.v
+src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v
 src/Specific/Framework/ArithmeticSynthesis/SquareFromMul.v
-src/Specific/NISTP256/AMD64/MontgomeryP256.v
+src/Specific/NISTP256/AMD128/CurveParameters.v
+src/Specific/NISTP256/AMD128/Synthesis.v
+src/Specific/NISTP256/AMD128/feadd.v
+src/Specific/NISTP256/AMD128/feaddDisplay.v
+src/Specific/NISTP256/AMD128/femul.v
+src/Specific/NISTP256/AMD128/femulDisplay.v
+src/Specific/NISTP256/AMD128/fenz.v
+src/Specific/NISTP256/AMD128/fenzDisplay.v
+src/Specific/NISTP256/AMD128/feopp.v
+src/Specific/NISTP256/AMD128/feoppDisplay.v
+src/Specific/NISTP256/AMD128/fesub.v
+src/Specific/NISTP256/AMD128/fesubDisplay.v
+src/Specific/NISTP256/AMD64/CurveParameters.v
+src/Specific/NISTP256/AMD64/Synthesis.v
 src/Specific/NISTP256/AMD64/feadd.v
 src/Specific/NISTP256/AMD64/feaddDisplay.v
 src/Specific/NISTP256/AMD64/femul.v