move src/Experiments/NewPipeline/ to src/

1 files changed, 38 insertions, 38 deletions

diff --git a/_CoqProject b/_CoqProject
index 77482ceb2..5cb9ea44c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -16,7 +16,38 @@ bbv/theories/Word.v
 bbv/theories/WordScope.v
 bbv/theories/ZHints.v
 bbv/theories/ZLib.v
+src/AbstractInterpretation.v
+src/AbstractInterpretationProofs.v
+src/AbstractInterpretationWf.v
+src/AbstractInterpretationZRangeProofs.v
+src/Arithmetic.v
+src/BoundsPipeline.v
+src/CLI.v
+src/COperationSpecifications.v
+src/CStringification.v
+src/CompilersTestCases.v
 src/Demo.v
+src/GENERATEDIdentifiersWithoutTypes.v
+src/GENERATEDIdentifiersWithoutTypesProofs.v
+src/Language.v
+src/LanguageInversion.v
+src/LanguageWf.v
+src/MiscCompilerPasses.v
+src/MiscCompilerPassesProofs.v
+src/PushButtonSynthesis.v
+src/Rewriter.v
+src/RewriterInterpProofs1.v
+src/RewriterProofs.v
+src/RewriterRulesGood.v
+src/RewriterRulesInterpGood.v
+src/RewriterWf1.v
+src/RewriterWf2.v
+src/SlowPrimeSynthesisExamples.v
+src/StandaloneHaskellMain.v
+src/StandaloneOCamlMain.v
+src/Toplevel2.v
+src/UnderLets.v
+src/UnderLetsProofs.v
 src/Algebra/Field.v
 src/Algebra/Field_test.v
 src/Algebra/Group.v
@@ -246,44 +277,12 @@ src/Curves/Weierstrass/Jacobian.v
 src/Curves/Weierstrass/Projective.v
 src/Experiments/PartialEvaluationWithLetIn.v
 src/Experiments/SimplyTypedArithmetic.v
-src/Experiments/NewPipeline/AbstractInterpretation.v
-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
-src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v
-src/Experiments/NewPipeline/Language.v
-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
-src/Experiments/NewPipeline/RewriterRulesGood.v
-src/Experiments/NewPipeline/RewriterRulesInterpGood.v
-src/Experiments/NewPipeline/RewriterWf1.v
-src/Experiments/NewPipeline/RewriterWf2.v
-src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v
-src/Experiments/NewPipeline/StandaloneHaskellMain.v
-src/Experiments/NewPipeline/StandaloneOCamlMain.v
-src/Experiments/NewPipeline/Toplevel2.v
-src/Experiments/NewPipeline/UnderLets.v
-src/Experiments/NewPipeline/UnderLetsProofs.v
-src/Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.v
-src/Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.v
-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/ExtractionHaskell/saturated_solinas.v
+src/ExtractionHaskell/unsaturated_solinas.v
+src/ExtractionHaskell/word_by_word_montgomery.v
+src/ExtractionOCaml/saturated_solinas.v
+src/ExtractionOCaml/unsaturated_solinas.v
+src/ExtractionOCaml/word_by_word_montgomery.v
 src/LegacyArithmetic/ArchitectureToZLike.v
 src/LegacyArithmetic/ArchitectureToZLikeProofs.v
 src/LegacyArithmetic/BarretReduction.v
@@ -311,6 +310,7 @@ src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
 src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v
 src/Primitives/EdDSARepChange.v
 src/Primitives/MxDHRepChange.v
+src/PushButtonSynthesis/ReificationCache.v
 src/Spec/CompleteEdwardsCurve.v
 src/Spec/Ed25519.v
 src/Spec/EdDSA.v