diff options
Diffstat (limited to 'src/PushButtonSynthesis/BarrettReductionReificationCache.v')
-rw-r--r-- | src/PushButtonSynthesis/BarrettReductionReificationCache.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/PushButtonSynthesis/BarrettReductionReificationCache.v b/src/PushButtonSynthesis/BarrettReductionReificationCache.v index 4c538087e..265ada2d2 100644 --- a/src/PushButtonSynthesis/BarrettReductionReificationCache.v +++ b/src/PushButtonSynthesis/BarrettReductionReificationCache.v @@ -14,15 +14,15 @@ Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBU Module Export BarrettReduction. (* all the list operations from for_reification.ident *) Strategy 100 [length seq repeat combine map flat_map partition app rev fold_right update_nth nth_default ]. - Strategy -10 [barrett_reduce reduce]. + Strategy -10 [Fancy.fancy_reduce reduce]. Derive reified_barrett_red_gen - SuchThat (is_reification_of reified_barrett_red_gen barrett_reduce) + SuchThat (is_reification_of reified_barrett_red_gen Fancy.fancy_reduce) As reified_barrett_red_gen_correct. Proof. Time cache_reify (). Time Qed. Module Export ReifyHints. - Hint Extern 1 (_ = _) => apply_cached_reification barrett_reduce (proj1 reified_barrett_red_gen_correct) : reify_cache_gen. + Hint Extern 1 (_ = _) => apply_cached_reification Fancy.fancy_reduce (proj1 reified_barrett_red_gen_correct) : reify_cache_gen. Hint Immediate (proj2 reified_barrett_red_gen_correct) : wf_gen_cache. Hint Rewrite (proj1 reified_barrett_red_gen_correct) : interp_gen_cache. End ReifyHints. |