From c98b81735cf3fa04a8897cf02c32a4b371a82ca9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 6 Jul 2018 15:47:10 -0400 Subject: Fix an infinite loop in Z.peel_le --- src/Util/ZUtil/Tactics/PeelLe.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util') 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 / _ ] -- cgit v1.2.3