1 files changed, 0 insertions, 34 deletions
diff --git a/src/Arithmetic/Saturated/UniformWeightInstances.v b/src/Arithmetic/Saturated/UniformWeightInstances.v
deleted file mode 100644
index 7ca7b1f3e..000000000
--- a/src/Arithmetic/Saturated/UniformWeightInstances.v
+++ /dev/null
@@ -1,34 +0,0 @@
-Require Import Coq.ZArith.BinInt.
-Require Import Crypto.Arithmetic.Saturated.UniformWeight.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.Decidable.
-Require Import Crypto.Util.Tactics.DestructHead.
-
-Fixpoint small_Decidable' {bound n} : forall (p : Tuple.tuple' Z n), Decidable (small (n:=S n) bound p).
-Proof.
-  refine match n as n return forall p : Tuple.tuple' Z n, id (Decidable (small (n:=S n) bound p)) with
-         | 0
-           => fun p : Z
-              => if dec (0 <= p < bound)%Z then left _ else right _
-         | S n'
-           => fun p : Tuple.tuple' Z n' * Z
-              => if dec (0 <= snd p < bound)%Z
-                 then if dec (small (n:=S n') bound (fst p))%Z
-                      then left _
-                      else right _
-                 else right _
-         end;
-    unfold id, small in *; simpl in *;
-      [ clear small_Decidable' n
-      | clear small_Decidable' n
-      | clear small_Decidable'; simpl in *.. ];
-      [ abstract (simpl in *; intros; destruct_head'_or; subst; auto; exfalso; assumption)
-      | abstract (simpl in *; intros; destruct_head'_or; subst; auto; exfalso; assumption)
-      | abstract (destruct p; simpl in *; intros; destruct_head'_or; subst; auto).. ].
-Defined.
-
-Global Instance small_Decidable {bound n} : forall (p : Tuple.tuple Z n), Decidable (small bound p).
-Proof.
-  destruct n; simpl; [ left | apply small_Decidable' ].
-  intros ??; exfalso; assumption.
-Defined.