1 files changed, 0 insertions, 13 deletions
diff --git a/src/Util/BoundedWord.v b/src/Util/BoundedWord.v
deleted file mode 100644
index e5c3720fe..000000000
--- a/src/Util/BoundedWord.v
+++ /dev/null
@@ -1,13 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.ZRange.
-Require Import Crypto.Util.FixedWordSizes.
-
-Definition BoundedWord n (bitwidth : nat)
-           (bounds : tuple zrange n) : Type :=
-  { x : tuple (wordT (Nat.log2 bitwidth)) n
-  | is_bounded_by None bounds
-                  (map wordToZ x)}.
-
-Definition BoundedWordToZ n w b (BW :BoundedWord n w b)
-  : tuple Z n :=  map wordToZ (proj1_sig BW).