diff options
Diffstat (limited to '_CoqProject')
-rw-r--r-- | _CoqProject | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject index ce927e75e..77482ceb2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -251,7 +251,9 @@ src/Experiments/NewPipeline/AbstractInterpretationProofs.v src/Experiments/NewPipeline/AbstractInterpretationWf.v src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v src/Experiments/NewPipeline/Arithmetic.v +src/Experiments/NewPipeline/BoundsPipeline.v src/Experiments/NewPipeline/CLI.v +src/Experiments/NewPipeline/COperationSpecifications.v src/Experiments/NewPipeline/CStringification.v src/Experiments/NewPipeline/CompilersTestCases.v src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v @@ -261,6 +263,7 @@ src/Experiments/NewPipeline/LanguageInversion.v src/Experiments/NewPipeline/LanguageWf.v src/Experiments/NewPipeline/MiscCompilerPasses.v src/Experiments/NewPipeline/MiscCompilerPassesProofs.v +src/Experiments/NewPipeline/PushButtonSynthesis.v src/Experiments/NewPipeline/Rewriter.v src/Experiments/NewPipeline/RewriterInterpProofs1.v src/Experiments/NewPipeline/RewriterProofs.v @@ -271,7 +274,6 @@ src/Experiments/NewPipeline/RewriterWf2.v src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v src/Experiments/NewPipeline/StandaloneHaskellMain.v src/Experiments/NewPipeline/StandaloneOCamlMain.v -src/Experiments/NewPipeline/Toplevel1.v src/Experiments/NewPipeline/Toplevel2.v src/Experiments/NewPipeline/UnderLets.v src/Experiments/NewPipeline/UnderLetsProofs.v @@ -281,6 +283,7 @@ src/Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.v src/Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.v src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.v src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.v +src/Experiments/NewPipeline/PushButtonSynthesis/ReificationCache.v src/LegacyArithmetic/ArchitectureToZLike.v src/LegacyArithmetic/ArchitectureToZLikeProofs.v src/LegacyArithmetic/BarretReduction.v |