1 files changed, 8 insertions, 6 deletions
diff --git a/_CoqProject b/_CoqProject
index 9dc26ab87..e141313b6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -229,12 +229,8 @@ src/Spec/MxDH.v
 src/Spec/WeierstrassCurve.v
 src/Spec/Test/X25519.v
 src/Specific/ArithmeticSynthesisTest130.v
-src/Specific/IntegrationTestFreeze.v
-src/Specific/IntegrationTestFreezeDisplay.v
 src/Specific/IntegrationTestKaratsubaMul.v
 src/Specific/IntegrationTestKaratsubaMulDisplay.v
-src/Specific/IntegrationTestLadderstep130.v
-src/Specific/IntegrationTestLadderstep130Display.v
 src/Specific/IntegrationTestMontgomeryP256_128.v
 src/Specific/IntegrationTestMontgomeryP256_128Display.v
 src/Specific/IntegrationTestMontgomeryP256_128_Add.v
@@ -245,8 +241,6 @@ 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/IntegrationTestSub.v
-src/Specific/IntegrationTestSubDisplay.v
 src/Specific/Karatsuba.v
 src/Specific/MontgomeryP256_128.v
 src/Specific/Framework/ArithmeticSynthesisFramework.v
@@ -277,14 +271,22 @@ 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/C32/freeze.v
+src/Specific/X25519/C32/freezeDisplay.v
 src/Specific/X25519/C64/CurveParameters.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
 src/Specific/X25519/C64/fesquareDisplay.v
+src/Specific/X25519/C64/freeze.v
+src/Specific/X25519/C64/freezeDisplay.v
 src/Specific/X25519/C64/ladderstep.v
 src/Specific/X25519/C64/ladderstepDisplay.v
+src/Specific/X2555/C128/CurveParameters.v
+src/Specific/X2555/C128/Synthesis.v
+src/Specific/X2555/C128/ladderstep.v
+src/Specific/X2555/C128/ladderstepDisplay.v
 src/Util/AdditionChainExponentiation.v
 src/Util/AutoRewrite.v
 src/Util/Bool.v