diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-17 15:07:47 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-18 19:44:48 -0500 |
| commit | cdd5ffb086eb647eabe640c81de9d8af7cd0a1dd (patch) | |
| tree | 4540df27da661c35fdc5246f1692fa124003ff6f /_CoqProject | |
| parent | b99dd6da3b6370bc225d3b501bda07c49fd29c12 (diff) | |
Split up PushButtonSynthesis.v
Closes #497
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 |