From 174fd1f853f47d24b350a53e7f186ab37829dc2a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 4 May 2016 12:08:30 +0200
Subject: Int.v: simplify Jason's commit 5b4e3ace

---
 theories/ZArith/Int.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index b78891c711..143d3c8dbe 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -452,7 +452,7 @@ Module Z_as_Int <: Int.
   Proof. reflexivity. Qed.
 
   (** Compatibility notations for Coq v8.4 *)
-  Notation plus := Coq.ZArith.Int.Z_as_Int.add (compat "8.4").
-  Notation minus := Coq.ZArith.Int.Z_as_Int.sub (compat "8.4").
-  Notation mult := Coq.ZArith.Int.Z_as_Int.mul (compat "8.4").
+  Notation plus := add (compat "8.4").
+  Notation minus := sub (compat "8.4").
+  Notation mult := mul (compat "8.4").
 End Z_as_Int.
-- 
cgit v1.2.3