From ff7be36add22cf3c6efd24a27ebdde818fc1dc06 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
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/FSets/FMapFacts.v          | 4 ++--
 theories/Reals/RIneq.v              | 2 +-
 theories/Reals/Rbasic_fun.v         | 2 +-
 theories/Reals/Rlogic.v             | 4 ++--
 theories/Structures/OrderedTypeEx.v | 2 +-
 5 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'theories')

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index ef852a98d..5ae22c497 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -440,7 +440,7 @@ destruct (eq_dec x y); auto.
 Qed.
 
 Lemma map_o : forall m x (f:elt->elt'),
- find x (map f m) = option_map f (find x m).
+ find x (map f m) = Datatypes.option_map f (find x m).
 Proof.
 intros.
 generalize (find_mapsto_iff (map f m) x) (find_mapsto_iff m x)
@@ -473,7 +473,7 @@ Qed.
 
 Lemma mapi_o : forall m x (f:key->elt->elt'),
  (forall x y e, E.eq x y -> f x e = f y e) ->
- find x (mapi f m) = option_map (f x) (find x m).
+ find x (mapi f m) = Datatypes.option_map (f x) (find x m).
 Proof.
 intros.
 generalize (find_mapsto_iff (mapi f m) x) (find_mapsto_iff m x)
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index bc82c3712..ab7fa15d2 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -2027,7 +2027,7 @@ Qed.
 
 Lemma R_rm : ring_morph
   0%R 1%R Rplus Rmult Rminus Ropp eq
-  0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool IZR.
+  0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR.
 Proof.
 constructor ; try easy.
 exact plus_IZR.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 17b3c5099..a50c7f952 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.
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index 4ad3339ec..c1b479b61 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -63,7 +63,7 @@ destruct (Rle_lt_dec l 0) as [Hl|Hl].
   now apply Rinv_0_lt_compat.
   now apply Hnp.
 left.
-set (N := Zabs_nat (up (/l) - 2)).
+set (N := Z.abs_nat (up (/l) - 2)).
 assert (H1l: (1 <= /l)%R).
   rewrite <- Rinv_1.
   apply Rinv_le_contravar with (1 := Hl).
@@ -75,7 +75,7 @@ assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R).
   rewrite inj_Zabs_nat.
   replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R.
   apply (f_equal (fun v => IZR v + 1)%R).
-  apply Zabs_eq.
+  apply Z.abs_eq.
   apply Zle_minus_le_0.
   apply (Zlt_le_succ 1).
   apply lt_IZR.
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index 3c6afc7b2..9b004a6da 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -55,7 +55,7 @@ Module Nat_as_OT <: UsualOrderedType.
 
   Definition compare x y : Compare lt eq x y.
   Proof.
-    case_eq (nat_compare x y); intro.
+    case_eq (Nat.compare x y); intro.
     - apply EQ. now apply nat_compare_eq.
     - apply LT. now apply nat_compare_Lt_lt.
     - apply GT. now apply nat_compare_Gt_gt.
-- 
cgit v1.2.3