From d20b2cbc862fb35b5e059cbfafaaa9360fb6afce Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@google.com>
Date: Fri, 26 Apr 2019 16:33:54 -0400
Subject: Remove BoundedWord

Remove Util/BoundedWord.v and its reverse dependencies
Util/FixedWordSizes.v and Util/FixedWordSizesEquality.v. This code is no
longer in use.
---
 src/Util/BoundedWord.v | 13 -------------
 1 file changed, 13 deletions(-)
 delete mode 100644 src/Util/BoundedWord.v

(limited to 'src/Util/BoundedWord.v')

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).
-- 
cgit v1.2.3