1 files changed, 0 insertions, 49 deletions
diff --git a/src/RewriterFull.v b/src/RewriterFull.v
deleted file mode 100644
index 772732442..000000000
--- a/src/RewriterFull.v
+++ /dev/null
@@ -1,49 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Util.ZRange.
-Require Import Crypto.RewriterRules.
-Require Import Crypto.Rewriter.
-Local Open Scope Z_scope.
-
-Import Compilers.RewriteRules.GoalType.
-Import Compilers.RewriteRules.Tactic.
-
-Module Compilers.
-  Module RewriteRules.
-    Definition RewriterNBE : RewriterT.
-    Proof. make_Rewriter true nbe_rewrite_rulesT. Defined.
-
-    Definition RewriterArith (max_const_val : Z) : RewriterT.
-    Proof. make_Rewriter false (arith_rewrite_rulesT max_const_val). Defined.
-
-    Definition RewriterArithWithCasts : RewriterT.
-    Proof. make_Rewriter false arith_with_casts_rewrite_rulesT. Defined.
-
-    Definition RewriterStripLiteralCasts : RewriterT.
-    Proof. make_Rewriter false strip_literal_casts_rewrite_rulesT. Defined.
-
-    Definition RewriterToFancy
-               (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z)
-      : RewriterT.
-    Proof. make_Rewriter false fancy_rewrite_rulesT. Defined.
-
-    Definition RewriterToFancyWithCasts
-               (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z)
-               (value_range flag_range : zrange)
-      : RewriterT.
-    Proof. make_Rewriter false (fancy_with_casts_rewrite_rulesT invert_low invert_high value_range flag_range). Defined.
-
-    Definition RewriteNBE {t} := Eval hnf in @Rewrite RewriterNBE t.
-    Definition RewriteArith max_const_val {t} := Eval hnf in @Rewrite (RewriterArith max_const_val) t.
-    Definition RewriteArithWithCasts {t} := Eval hnf in @Rewrite RewriterArithWithCasts t.
-    Definition RewriteStripLiteralCasts {t} := Eval hnf in @Rewrite RewriterStripLiteralCasts t.
-    Definition RewriteToFancy invert_low invert_high {t}
-      := Eval hnf in @Rewrite (RewriterToFancy invert_low invert_high) t.
-    Definition RewriteToFancyWithCasts invert_low invert_high value_range flag_range {t}
-      := Eval hnf in @Rewrite (RewriterToFancyWithCasts invert_low invert_high value_range flag_range) t.
-  End RewriteRules.
-
-  Import Language.Compilers.defaults.
-
-  Definition PartialEvaluate {t} (e : Expr t) : Expr t
-    := RewriteRules.RewriteNBE e.
-End Compilers.