diff options
| author |  jadep <jadep@mit.edu> | 2019-02-15 14:56:22 -0500 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-02-21 11:10:12 -0500 |
| commit | 9025014cf7b64082d0bfed93dd76ba99ab9bb72b (patch) | |
| tree | 9ef8dd60ee34fe50335b53b1b57f56bf39f84d47 /src/PushButtonSynthesis/BarrettReduction.v | |
| parent | a1f9d9ee2c662790b43bf56df58121a390efbe7c (diff) | |
Make Qed not take forever
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 |