From c0fe35f49d61207d16c6db79936e38edf9661a49 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 1 Apr 2019 05:38:38 -0400 Subject: rename some things --- .../MontgomeryReductionReificationCache.v | 23 ---------------------- 1 file changed, 23 deletions(-) delete mode 100644 src/PushButtonSynthesis/MontgomeryReductionReificationCache.v (limited to 'src/PushButtonSynthesis/MontgomeryReductionReificationCache.v') 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. -- cgit v1.2.3