From 1ecf2f9945a99b5e4a58ebe46ec5764f07ec05aa Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Wed, 14 Sep 2016 14:09:29 -0400
Subject: More 8.4 compatibility

---
 src/Util/ZUtil.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/Util')

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index abae9de41..ce473fcb4 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1681,7 +1681,8 @@ Module Z.
 
   Lemma lt_mul_2_mod_sub : forall a b, b <> 0 -> b <= a < 2 * b -> a mod b = a - b.
   Proof.
-    intros; replace a with (1 * b + (a - b)) at 1 by ring.
+    intros.
+    replace (a mod b) with ((1 * b + (a - b)) mod b) by (f_equal; ring).
     rewrite Z.mod_add_l by auto.
     apply Z.mod_small.
     omega.
-- 
cgit v1.2.3