From cdd5ffb086eb647eabe640c81de9d8af7cd0a1dd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 17 Jan 2019 15:07:47 -0500 Subject: Split up PushButtonSynthesis.v Closes #497 --- _CoqProject | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to '_CoqProject') 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 -- cgit v1.2.3