1 files changed, 0 insertions, 90 deletions
diff --git a/src/LegacyArithmetic/ZBoundedZ.v b/src/LegacyArithmetic/ZBoundedZ.v
deleted file mode 100644
index f0dfc6a40..000000000
--- a/src/LegacyArithmetic/ZBoundedZ.v
+++ /dev/null
@@ -1,90 +0,0 @@
-(*** ℤ can be a bounded ℤ-Like type *)
-Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.LegacyArithmetic.ZBounded.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Pow2Mod.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.Notations.
-
-Local Open Scope Z_scope.
-
-Global Instance ZZLikeOps small_bound_exp smaller_bound_exp modulus : ZLikeOps (2^small_bound_exp) (2^smaller_bound_exp) modulus
-  := { LargeT := Z;
-       SmallT := Z;
-       modulus_digits := modulus;
-       decode_large x := x;
-       decode_small x := x;
-       Mod_SmallBound x := Z.pow2_mod x small_bound_exp;
-       DivBy_SmallBound x := Z.shiftr x small_bound_exp;
-       DivBy_SmallerBound x := Z.shiftr x smaller_bound_exp;
-       Mul x y := (x * y)%Z;
-       CarryAdd x y := dlet xpy := x + y in
-                       ((2^small_bound_exp * 2^small_bound_exp <=? xpy), Z.pow2_mod xpy (2 * small_bound_exp));
-       CarrySubSmall x y := dlet xmy := x - y in (xmy <? 0, Z.pow2_mod xmy small_bound_exp);
-       ConditionalSubtract b x := dlet x := x in if b then Z.pow2_mod (x - modulus) small_bound_exp else x;
-       ConditionalSubtractModulus x := dlet x := x in if x <? modulus then x else x - modulus }.
-
-Local Arguments Z.mul !_ !_.
-
-Class cls_is_true (x : bool) := build_is_true : x = true.
-Hint Extern 1 (cls_is_true ?b) => vm_compute; reflexivity : typeclass_instances.
-
-Local Ltac pre_t :=
-  unfold cls_is_true, Let_In in *; Z.ltb_to_lt;
-  match goal with
-  | [ H : ?smaller_bound_exp <= ?small_bound_exp |- _ ]
-    => is_var smaller_bound_exp; is_var small_bound_exp;
-       assert (2^smaller_bound_exp <= 2^small_bound_exp) by auto with zarith;
-       assert (2^small_bound_exp * 2^smaller_bound_exp <= 2^small_bound_exp * 2^small_bound_exp) by auto with zarith
-  end.
-
-Local Ltac t_step :=
-  first [ progress simpl in *
-        | progress intros
-        | progress autorewrite with push_Zpow Zshift_to_pow in *
-        | rewrite Z.pow2_mod_spec by omega
-        | progress Z.ltb_to_lt
-        | progress unfold Let_In in *
-        | solve [ auto with zarith ]
-        | nia
-        | progress break_match ].
-Local Ltac t := pre_t; repeat t_step.
-
-Global Instance ZZLikeProperties {small_bound_exp smaller_bound_exp modulus}
-       {Hss : cls_is_true (0 <=? smaller_bound_exp)}
-       {Hs : cls_is_true (0 <=? small_bound_exp)}
-       {Hs_ss : cls_is_true (smaller_bound_exp <=? small_bound_exp)}
-       {Hmod0 : cls_is_true (0 <=? modulus)}
-       {Hmod1 : cls_is_true (modulus <? 2^small_bound_exp)}
-  : ZLikeProperties (@ZZLikeOps small_bound_exp smaller_bound_exp modulus).
-Proof.
-refine {| large_valid x := 0 <= x < 2^(2*small_bound_exp);
-          medium_valid x := 0 <= x < 2^(small_bound_exp + smaller_bound_exp);
-          small_valid x := 0 <= x < 2^small_bound_exp |}.
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-  { abstract t. }
-Defined.