1 files changed, 0 insertions, 23 deletions
diff --git a/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v b/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v
deleted file mode 100644
index 80af335df..000000000
--- a/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v
+++ /dev/null
@@ -1,23 +0,0 @@
-(** * Push-Button Synthesis of Saturated Solinas: Reification Cache *)
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.FancyMontgomeryReduction.
-Require Import Crypto.PushButtonSynthesis.ReificationCache.
-Local Open Scope Z_scope.
-
-Import Associational Positional Arithmetic.MontgomeryReduction.
-
-Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *)
-
-Module Export MontgomeryReduction.
-  Derive reified_montred_gen
-         SuchThat (is_reification_of reified_montred_gen montred')
-         As reified_montred_gen_correct.
-  Proof. Time cache_reify (). Time Qed.
-  Module Export ReifyHints.
-    Hint Extern 1 (_ = _) => apply_cached_reification montred' (proj1 reified_montred_gen_correct) : reify_cache_gen.
-    Hint Immediate (proj2 reified_montred_gen_correct) : wf_gen_cache.
-    Hint Rewrite (proj1 reified_montred_gen_correct) : interp_gen_cache.
-  End ReifyHints.
-  Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *)
-End MontgomeryReduction.