diff options
Diffstat (limited to 'src/PushButtonSynthesis/BarrettReduction.v')
| -rw-r--r-- | src/PushButtonSynthesis/BarrettReduction.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v index bc525412a..224584c4a 100644 --- a/src/PushButtonSynthesis/BarrettReduction.v +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -96,6 +96,7 @@ Section rbarrett_red. prefix "barrett_red" barrett_red (fun _ _ _ => @nil string). + Local Strategy -100 [barrett_red]. (* Probably needed to make Qed not take forever *) (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like << Lemma barrett_red_correct res |