4 files changed, 3 insertions, 3 deletions
diff --git a/_CoqProject b/_CoqProject
index 8c376eb88..44f15cb76 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -240,7 +240,6 @@ src/Curves/Weierstrass/Affine.v
 src/Curves/Weierstrass/AffineProofs.v
 src/Curves/Weierstrass/Jacobian.v
 src/Curves/Weierstrass/Projective.v
-src/Experiments/Loops.v
 src/Experiments/SimplyTypedArithmetic.v
 src/LegacyArithmetic/ArchitectureToZLike.v
 src/LegacyArithmetic/ArchitectureToZLikeProofs.v
@@ -6465,6 +6464,7 @@ src/Util/LetIn.v
 src/Util/LetInMonad.v
 src/Util/ListUtil.v
 src/Util/Logic.v
+src/Util/Loops.v
 src/Util/NUtil.v
 src/Util/NatUtil.v
 src/Util/Notations.v
diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v
index 336ee6b95..88e1d7398 100644
--- a/src/Curves/Montgomery/XZ.v
+++ b/src/Curves/Montgomery/XZ.v
@@ -2,7 +2,7 @@ Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations.
 Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn.
 Require Import Crypto.Util.Decidable.
-Require Import Crypto.Experiments.Loops.
+Require Import Crypto.Util.Loops.
 Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine.
 
 Module M.
diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v
index f44e5fc33..650ed6920 100644
--- a/src/Curves/Montgomery/XZProofs.v
+++ b/src/Curves/Montgomery/XZProofs.v
@@ -258,7 +258,7 @@ Module M.
     Local Notation montladder := (M.montladder(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)(Fzero:=Fzero)(Fone:=Fone)(Finv:=Finv)(cswap:=fun b x y => if b then pair y x else pair x y)).
     Local Notation scalarmult := (@ScalarMult.scalarmult_ref Mpoint Madd M.zero Mopp).
 
-    Import Crypto.Experiments.Loops.
+    Import Crypto.Util.Loops.
     Import Coq.ZArith.BinInt.
 
     Lemma to_x_inv00 (HFinv:Finv 0 = 0) x z : to_x (pair x z) = x * Finv z.
diff --git a/src/Experiments/Loops.v b/src/Util/Loops.v
index 56b27dac7..56b27dac7 100644
--- a/src/Experiments/Loops.v
+++ b/src/Util/Loops.v