From 430cf3778555fd9dfef5dccb3f57052df994cbc4 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 2 Aug 2018 18:16:45 +0100
Subject: Coq mips: fix deprecation warning

---
 mips/mips_extras.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mips/mips_extras.v b/mips/mips_extras.v
index 8ca4546c..626b4109 100644
--- a/mips/mips_extras.v
+++ b/mips/mips_extras.v
@@ -143,7 +143,7 @@ Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0
 refine (existT _ (ZEuclid.modulo m n) _).
 constructor.
 destruct H.
-assert (Zabs n = n). { rewrite Zabs_eq; auto with zarith. }
+assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. }
 rewrite <- H at 3.
 lapply (ZEuclid.mod_always_pos m n); omega.
 Qed.
-- 
cgit v1.2.3