Move FancyMachine from Experiments to Specific

Quoting Andres:
> I am leaning towards putting this in Specifc instead of Experiments -- it
> seems like complete result on its own, these files are unlikely to be reused
> for something else, and I don't think we are expecting to need to remove it
> any time soon. Currently, `Specific` code does not quantify over anything (no
> context variables), but this seems secondary. We could make versions of this
> with the curve constants plugged in, though.

3 files changed, 2 insertions, 2 deletions

diff --git a/src/Experiments/FancyMachineBarrett256.v b/src/Specific/FancyMachine256/Barrett.v
index 0243c284f..1683522e3 100644
--- a/src/Experiments/FancyMachineBarrett256.v
+++ b/src/Specific/FancyMachine256/Barrett.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Experiments.FancyMachine256.
+Require Import Crypto.Specific.FancyMachine256.Core.
 Require Import Crypto.ModularArithmetic.BarrettReduction.ZBounded.
 Require Import Crypto.ModularArithmetic.BarrettReduction.ZHandbook.
 
diff --git a/src/Experiments/FancyMachine256.v b/src/Specific/FancyMachine256/Core.v
index d11cfe6ad..d11cfe6ad 100644
--- a/src/Experiments/FancyMachine256.v
+++ b/src/Specific/FancyMachine256/Core.v
diff --git a/src/Experiments/FancyMachineMontgomery256.v b/src/Specific/FancyMachine256/Montgomery.v
index 0f8d8bd59..a9a50f773 100644
--- a/src/Experiments/FancyMachineMontgomery256.v
+++ b/src/Specific/FancyMachine256/Montgomery.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Experiments.FancyMachine256.
+Require Import Crypto.Specific.FancyMachine256.Core.
 Require Import Crypto.ModularArithmetic.Montgomery.ZBounded.
 Require Import Crypto.ModularArithmetic.Montgomery.ZProofs.