From ff7be36add22cf3c6efd24a27ebdde818fc1dc06 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 20 Feb 2018 14:10:58 +0100
Subject: Turn warning for deprecated notations on.

Fix new deprecation warnings in the standard library.
---
 theories/Reals/Rbasic_fun.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Reals/Rbasic_fun.v')

diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 17b3c5099a..a50c7f9523 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -609,7 +609,7 @@ Qed.
 
 Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Z.abs z).
 Proof.
-  intros z; case z; unfold Zabs.
+  intros z; case z; unfold Z.abs.
   apply Rabs_R0.
   now intros p0; apply Rabs_pos_eq, (IZR_le 0).
   unfold IZR at 1.
-- 
cgit v1.2.3