diff options
| author |  Jason Gross <jagro@google.com> | 2018-07-06 15:47:10 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-07-06 15:52:34 -0400 |
| commit | c98b81735cf3fa04a8897cf02c32a4b371a82ca9 (patch) | |
| tree | 3770d292e4566a18011bbe04a3586b496f261f38 /src/Util/ZUtil | |
| parent | 2a7c3b95ea4fe28a6c4cd1c5b12e3bdbb6b75204 (diff) | |
Fix an infinite loop in Z.peel_le
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/Tactics/PeelLe.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Tactics/PeelLe.v b/src/Util/ZUtil/Tactics/PeelLe.v index f299e0acd..11ae2f87d 100644 --- a/src/Util/ZUtil/Tactics/PeelLe.v +++ b/src/Util/ZUtil/Tactics/PeelLe.v @@ -33,7 +33,7 @@ Module Z. => first [ apply Z.mul_le_mono_nonneg_r; [ zutil_arith | ] | apply Z.mul_le_mono_nonpos_r; [ zutil_arith | ] ] | [ |- -_ <= -_ ] - => apply Z.opp_le_mono + => apply -> Z.opp_le_mono | [ |- _ / ?x <= _ / ?x ] => apply Z.div_le_mono; [ zutil_arith | ] | [ |- ?x / _ <= ?x / _ ] |