diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-06-18 15:46:40 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-06-18 15:47:33 -0400 |
| commit | 87bf48fccf89460b8264bb5cedf6b0e966dde563 (patch) | |
| tree | 4222fdb4f6e3b496623b28a26e994f07154e1a47 /_CoqProject | |
| parent | 989f6a49cb390b6279ee8ce0ed70eb993ff1b809 (diff) | |
compile X25519 C code from Makefile
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/_CoqProject b/_CoqProject index 54d4958b2..f82134709 100644 --- a/_CoqProject +++ b/_CoqProject @@ -221,18 +221,12 @@ src/Specific/IntegrationTestFreeze.v src/Specific/IntegrationTestFreezeDisplay.v src/Specific/IntegrationTestKaratsubaMul.v src/Specific/IntegrationTestKaratsubaMulDisplay.v -src/Specific/IntegrationTestLadderstep.v src/Specific/IntegrationTestLadderstep130.v src/Specific/IntegrationTestLadderstep130Display.v -src/Specific/IntegrationTestLadderstepDisplay.v src/Specific/IntegrationTestMontgomeryP256.v src/Specific/IntegrationTestMontgomeryP256Display.v src/Specific/IntegrationTestMontgomeryP256_128.v src/Specific/IntegrationTestMontgomeryP256_128Display.v -src/Specific/IntegrationTestMul.v -src/Specific/IntegrationTestMulDisplay.v -src/Specific/IntegrationTestSquare.v -src/Specific/IntegrationTestSquareDisplay.v src/Specific/IntegrationTestSub.v src/Specific/IntegrationTestSubDisplay.v src/Specific/IntegrationTestTemporaryMiscCommon.v @@ -242,6 +236,12 @@ src/Specific/MontgomeryP256_128.v src/Specific/FancyMachine256/Barrett.v src/Specific/FancyMachine256/Core.v src/Specific/FancyMachine256/Montgomery.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/ladderstep.v +src/Specific/X25519/C64/ladderstepDisplay.v src/Util/AdditionChainExponentiation.v src/Util/AutoRewrite.v src/Util/Bool.v |