Commit 99ac25e2 by Guillaume Melquiond

### Eliminate some more deprecation warnings.

parent 81831def
 ... ... @@ -74,7 +74,7 @@ rewrite H1; unfold F2R; simpl. rewrite bpow_plus, bpow_1. simpl;ring. easy. apply Zle_trans with (1:=H3). apply Z.le_trans with (1:=H3). apply Zle_succ. Qed. ... ...
 ... ... @@ -55,7 +55,7 @@ Qed. Definition plus (x y : float beta) := let (m, e) := Fplus x y in let s := Zlt_bool m 0 in let '(m', e', l) := truncate beta fexp (Zabs m, e, loc_Exact) in let '(m', e', l) := truncate beta fexp (Z.abs m, e, loc_Exact) in Float beta (cond_Zopp s (choice s m' l)) e'. Theorem plus_correct : ... ... @@ -66,7 +66,7 @@ intros x y. unfold plus. rewrite <- F2R_plus. destruct (Fplus x y) as [m e]. rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Zabs m) e loc_Exact). rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Z.abs m) e loc_Exact). 3: now right. destruct truncate as [[m' e'] l']. apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))). ... ... @@ -78,7 +78,7 @@ Qed. Definition mult (x y : float beta) := let (m, e) := Fmult x y in let s := Zlt_bool m 0 in let '(m', e', l) := truncate beta fexp (Zabs m, e, loc_Exact) in let '(m', e', l) := truncate beta fexp (Z.abs m, e, loc_Exact) in Float beta (cond_Zopp s (choice s m' l)) e'. Theorem mult_correct : ... ... @@ -89,7 +89,7 @@ intros x y. unfold mult. rewrite <- F2R_mult. destruct (Fmult x y) as [m e]. rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Zabs m) e loc_Exact). rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Z.abs m) e loc_Exact). 3: now right. destruct truncate as [[m' e'] l']. apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))). ... ...
 ... ... @@ -72,13 +72,13 @@ Lemma midpoint_beta_odd_remains_pos : Proof. intros x Px ex1 ex2 Hf2. set (z := (ex1 - ex2)%Z). assert (Hz : Z_of_nat (Zabs_nat z) = z). assert (Hz : Z_of_nat (Z.abs_nat z) = z). { rewrite Zabs2Nat.id_abs. rewrite <- cond_Zopp_Zlt_bool; unfold cond_Zopp. assert (H : (z
 ... ... @@ -99,8 +99,8 @@ Qed. Lemma FLXN_le_exp: forall f1 f2:float beta, ((Zpower beta (prec - 1) <= Zabs (Fnum f1) < Zpower beta prec)%Z) -> ((Zpower beta (prec - 1) <= Zabs (Fnum f2) < Zpower beta prec))%Z -> ((Zpower beta (prec - 1) <= Z.abs (Fnum f1) < Zpower beta prec)%Z) -> ((Zpower beta (prec - 1) <= Z.abs (Fnum f2) < Zpower beta prec))%Z -> 0 <= F2R f1 -> F2R f1 <= F2R f2 -> (Fexp f1 <= Fexp f2)%Z. Proof. intros f1 f2 H1 H2 H3 H4. ... ... @@ -132,7 +132,7 @@ apply Rmult_le_compat_r. apply bpow_ge_0. rewrite <- IZR_Zpower. apply IZR_le. apply Zle_trans with (1:=proj1 H1). apply Z.le_trans with (1:=proj1 H1). rewrite Z.abs_eq. auto with zarith. apply le_IZR. ... ... @@ -2177,7 +2177,7 @@ apply Rmult_le_compat_r. apply bpow_ge_0. rewrite <- IZR_Zpower. left; apply IZR_lt. replace (Fnum (Fabs f)) with (Zabs (Fnum f)). replace (Fnum (Fabs f)) with (Z.abs (Fnum f)). assumption. destruct f; unfold Fabs; reflexivity. omega. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!