1 files changed, 0 insertions, 42 deletions
diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v
deleted file mode 100644
index 2d3ed96e2..000000000
--- a/src/RewriterRulesGood.v
+++ /dev/null
@@ -1,42 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.RewriterFull.
-Require Import Crypto.RewriterWf1.
-Local Open Scope Z_scope.
-
-Module Compilers.
-  Import RewriterFull.Compilers.
-  Import RewriterWf1.Compilers.
-
-  Module Import RewriteRules.
-    Import RewriterFull.Compilers.RewriteRules.
-    Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType.
-    Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic.
-
-    Lemma RewriterRulesNBEWf : Wf_GoalT RewriterNBE.
-    Proof. prove_good (). Qed.
-
-    Lemma RewriterRulesArithWf max_const : Wf_GoalT (RewriterArith max_const).
-    Proof. prove_good (). Qed.
-
-    Lemma RewriterRulesArithWithCastsWf : Wf_GoalT RewriterArithWithCasts.
-    Proof. prove_good (). Qed.
-
-    Lemma RewriterRulesStripLiteralCastsWf : Wf_GoalT RewriterStripLiteralCasts.
-    Proof. prove_good (). Qed.
-
-    Lemma RewriterRulesToFancyWf
-            (invert_low invert_high : Z -> Z -> option Z)
-            (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
-            (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
-      : Wf_GoalT (RewriterToFancy invert_low invert_high).
-    Proof. prove_good (). Qed.
-
-    Lemma RewriterRulesToFancyWithCastsWf
-          (invert_low invert_high : Z -> Z -> option Z)
-          (value_range flag_range : ZRange.zrange)
-          (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
-          (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
-      : Wf_GoalT (RewriterToFancyWithCasts invert_low invert_high value_range flag_range).
-    Proof. prove_good (). Qed.
-  End RewriteRules.
-End Compilers.