1 files changed, 0 insertions, 18 deletions
diff --git a/src/LegacyArithmetic/Pow2Base.v b/src/LegacyArithmetic/Pow2Base.v
deleted file mode 100644
index c5c69e684..000000000
--- a/src/LegacyArithmetic/Pow2Base.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith.
-Require Import Crypto.Util.ListUtil.
-Require Import Coq.Lists.List.
-
-Local Open Scope Z_scope.
-
-Section Pow2Base.
-  Context (limb_widths : list Z).
-  Local Notation "w[ i ]" := (nth_default 0 limb_widths i).
-  Fixpoint base_from_limb_widths limb_widths :=
-    match limb_widths with
-    | nil => nil
-    | w :: lw => 1 :: map (Z.mul (two_p w)) (base_from_limb_widths lw)
-    end.
-  Local Notation base := (base_from_limb_widths limb_widths).
-  Definition bounded us := forall i, 0 <= nth_default 0 us i < 2 ^ w[i].
-  Definition upper_bound := 2 ^ (sum_firstn limb_widths (length limb_widths)).
-End Pow2Base.