diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-07-02 17:09:09 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-07-02 17:09:09 -0400 |
| commit | d7ad9528319596298b80e450e5a2eb87610d2fcf (patch) | |
| tree | 517a2de4683a867a706af0e3ee1e5f8ed164002c /_CoqProject | |
| parent | 448af3b44af491738b83a6084161e414d6522cdf (diff) | |
automate P256 integration
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/_CoqProject b/_CoqProject index d46c94a1f..aadb4a93d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -18,13 +18,6 @@ src/Arithmetic/Karatsuba.v src/Arithmetic/ModularArithmeticPre.v src/Arithmetic/ModularArithmeticTheorems.v src/Arithmetic/PrimeFieldTheorems.v -src/Arithmetic/Saturated/AddSub.v -src/Arithmetic/Saturated/Core.v -src/Arithmetic/Saturated/Freeze.v -src/Arithmetic/Saturated/MontgomeryAPI.v -src/Arithmetic/Saturated/MulSplit.v -src/Arithmetic/Saturated/UniformWeight.v -src/Arithmetic/Saturated/Wrappers.v src/Arithmetic/BarrettReduction/Generalized.v src/Arithmetic/BarrettReduction/HAC.v src/Arithmetic/BarrettReduction/Wikipedia.v @@ -36,6 +29,13 @@ src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition.v src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v +src/Arithmetic/Saturated/AddSub.v +src/Arithmetic/Saturated/Core.v +src/Arithmetic/Saturated/Freeze.v +src/Arithmetic/Saturated/MontgomeryAPI.v +src/Arithmetic/Saturated/MulSplit.v +src/Arithmetic/Saturated/UniformWeight.v +src/Arithmetic/Saturated/Wrappers.v src/Compilers/CommonSubexpressionElimination.v src/Compilers/CommonSubexpressionEliminationDenote.v src/Compilers/CommonSubexpressionEliminationInterp.v @@ -246,17 +246,17 @@ src/Specific/IntegrationTestSubDisplay.v src/Specific/IntegrationTestTemporaryMiscCommon.v src/Specific/Karatsuba.v src/Specific/MontgomeryP256_128.v -src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.v -src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.v -src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Add.v -src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.v -src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Nonzero.v -src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_NonzeroDisplay.v -src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Opp.v -src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.v -src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Sub.v -src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.v src/Specific/NISTP256/AMD64/MontgomeryP256.v +src/Specific/NISTP256/AMD64/feadd.v +src/Specific/NISTP256/AMD64/feaddDisplay.v +src/Specific/NISTP256/AMD64/femul.v +src/Specific/NISTP256/AMD64/femulDisplay.v +src/Specific/NISTP256/AMD64/fenz.v +src/Specific/NISTP256/AMD64/fenzDisplay.v +src/Specific/NISTP256/AMD64/feopp.v +src/Specific/NISTP256/AMD64/feoppDisplay.v +src/Specific/NISTP256/AMD64/fesub.v +src/Specific/NISTP256/AMD64/fesubDisplay.v src/Specific/NISTP256/FancyMachine256/Barrett.v src/Specific/NISTP256/FancyMachine256/Core.v src/Specific/NISTP256/FancyMachine256/Montgomery.v |