aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject5
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