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/RIneq.v | 2 +- theories/Reals/Rbasic_fun.v | 2 +- theories/Reals/Rlogic.v | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'theories/Reals') 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. -- cgit v1.2.3