diff options
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject index 80ff80d44..23bccf874 100644 --- a/_CoqProject +++ b/_CoqProject @@ -34,7 +34,6 @@ src/LanguageInversion.v src/LanguageWf.v src/MiscCompilerPasses.v src/MiscCompilerPassesProofs.v -src/PushButtonSynthesis.v src/Rewriter.v src/RewriterInterpProofs1.v src/RewriterProofs.v @@ -92,7 +91,21 @@ src/Fancy/Prod.v src/Fancy/Spec.v src/Primitives/EdDSARepChange.v src/Primitives/MxDHRepChange.v +src/PushButtonSynthesis/BarrettReduction.v +src/PushButtonSynthesis/BarrettReductionReificationCache.v +src/PushButtonSynthesis/InvertHighLow.v +src/PushButtonSynthesis/LegacySynthesisTactics.v +src/PushButtonSynthesis/MontgomeryReduction.v +src/PushButtonSynthesis/MontgomeryReductionReificationCache.v +src/PushButtonSynthesis/Primitives.v src/PushButtonSynthesis/ReificationCache.v +src/PushButtonSynthesis/SaturatedSolinas.v +src/PushButtonSynthesis/SaturatedSolinasReificationCache.v +src/PushButtonSynthesis/SmallExamples.v +src/PushButtonSynthesis/UnsaturatedSolinas.v +src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v +src/PushButtonSynthesis/WordByWordMontgomery.v +src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v src/Spec/CompleteEdwardsCurve.v src/Spec/Ed25519.v src/Spec/EdDSA.v |