diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-22 19:53:06 +0200 |
commit | 8d5c6bb8f0cac1339dec7b730997ee30b1517073 (patch) | |
tree | 3ffd8bcb28a88ae4ff51989aed37b0ad2cb676b2 /lib/Floats.v | |
parent | 0f210f622a4609811959f4450f770c61f5eb6532 (diff) | |
download | compcert-8d5c6bb8f0cac1339dec7b730997ee30b1517073.tar.gz compcert-8d5c6bb8f0cac1339dec7b730997ee30b1517073.zip |
Remove coq warnings (#28)
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
Diffstat (limited to 'lib/Floats.v')
-rw-r--r-- | lib/Floats.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index aa52b197..0c8ff5a4 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -92,10 +92,10 @@ Proof. destruct x as [[]|]; simpl; intros; discriminate. Qed. -Local Notation __ := (refl_equal Datatypes.Lt). +Local Notation __ := (eq_refl Datatypes.Lt). -Local Hint Extern 1 (Prec_gt_0 _) => exact (refl_equal Datatypes.Lt). -Local Hint Extern 1 (_ < _) => exact (refl_equal Datatypes.Lt). +Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt). +Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt). (** * Double-precision FP numbers *) @@ -266,13 +266,13 @@ Ltac compute_this val := let x := fresh in set val as x in *; vm_compute in x; subst x. Ltac smart_omega := - simpl radix_val in *; simpl Zpower in *; + simpl radix_val in *; simpl Z.pow in *; compute_this Int.modulus; compute_this Int.half_modulus; compute_this Int.max_unsigned; compute_this Int.min_signed; compute_this Int.max_signed; compute_this Int64.modulus; compute_this Int64.half_modulus; compute_this Int64.max_unsigned; - compute_this (Zpower_pos 2 1024); compute_this (Zpower_pos 2 53); compute_this (Zpower_pos 2 52); compute_this (Zpower_pos 2 32); + compute_this (Z.pow_pos 2 1024); compute_this (Z.pow_pos 2 53); compute_this (Z.pow_pos 2 52); compute_this (Z.pow_pos 2 32); zify; omega. (** Commutativity properties of addition and multiplication. *) @@ -510,10 +510,10 @@ Proof. intros; unfold from_words, of_bits, b64_of_bits, binary_float_of_bits. rewrite B2R_FF2B, is_finite_FF2B, Bsign_FF2B. unfold binary_float_of_bits_aux; rewrite split_bits_or; simpl; pose proof (Int.unsigned_range x). - destruct (Int.unsigned x + Zpower_pos 2 52) eqn:?. + destruct (Int.unsigned x + Z.pow_pos 2 52) eqn:?. exfalso; now smart_omega. simpl; rewrite <- Heqz; unfold F2R; simpl. split; auto. - rewrite <- (Z2R_plus 4503599627370496), Rmult_1_r. f_equal. rewrite Zplus_comm. auto. + rewrite <- (Z2R_plus 4503599627370496), Rmult_1_r. f_equal. rewrite Z.add_comm. auto. exfalso; now smart_omega. Qed. @@ -593,11 +593,11 @@ Proof. intros; unfold from_words, of_bits, b64_of_bits, binary_float_of_bits. rewrite B2R_FF2B, is_finite_FF2B, Bsign_FF2B. unfold binary_float_of_bits_aux; rewrite split_bits_or'; simpl; pose proof (Int.unsigned_range x). - destruct (Int.unsigned x + Zpower_pos 2 52) eqn:?. + destruct (Int.unsigned x + Z.pow_pos 2 52) eqn:?. exfalso; now smart_omega. simpl; rewrite <- Heqz; unfold F2R; simpl. split; auto. rewrite <- (Z2R_plus 19342813113834066795298816), <- (Z2R_mult _ 4294967296). - f_equal; compute_this (Zpower_pos 2 52); compute_this (two_power_pos 32); ring. + f_equal; compute_this (Z.pow_pos 2 52); compute_this (two_power_pos 32); ring. assert (Zneg p < 0) by reflexivity. exfalso; now smart_omega. Qed. @@ -807,10 +807,10 @@ Proof. rewrite BofZ_mult_2p. - change (2^1) with 2. rewrite EQ. apply BofZ_round_odd with (p := 1). + omega. -+ apply Zle_trans with Int64.modulus; trivial. smart_omega. ++ apply Z.le_trans with Int64.modulus; trivial. smart_omega. + omega. -+ apply Zle_trans with (2^63). compute; intuition congruence. xomega. -- apply Zle_trans with Int64.modulus; trivial. ++ apply Z.le_trans with (2^63). compute; intuition congruence. xomega. +- apply Z.le_trans with Int64.modulus; trivial. pose proof (Int64.signed_range n). compute_this Int64.min_signed; compute_this Int64.max_signed; compute_this Int64.modulus; xomega. @@ -1191,7 +1191,7 @@ Proof. assert (E: forall i, p < i -> Z.testbit m i = false). { intros. apply Z.testbit_false. omega. replace (m / 2^i) with 0. auto. symmetry. apply Zdiv_small. - unfold m. split. omega. apply Zlt_le_trans with (2 * 2^p). omega. + unfold m. split. omega. apply Z.lt_le_trans with (2 * 2^p). omega. change 2 with (2^1) at 1. rewrite <- (Zpower_plus radix2) by omega. apply Zpower_le. omega. } assert (F: forall i, 0 <= i -> Z.testbit (-2^p) i = if zlt i p then false else true). @@ -1222,7 +1222,7 @@ Proof. rewrite Bconv_BofZ. apply BofZ_round_odd with (p := 11). omega. - apply Zle_trans with (2^64). omega. compute; intuition congruence. + apply Z.le_trans with (2^64). omega. compute; intuition congruence. omega. exact (proj1 H). unfold int_round_odd. apply integer_representable_n2p_wide. auto. omega. @@ -1260,7 +1260,7 @@ Proof. assert (0 <= n'). { rewrite <- H1. change 0 with (int_round_odd 0 11). apply (int_round_odd_le 0 0); omega. } assert (n' < Int64.modulus). - { apply Zle_lt_trans with (int_round_odd (Int64.modulus - 1) 11). + { apply Z.le_lt_trans with (int_round_odd (Int64.modulus - 1) 11). rewrite <- H1. apply (int_round_odd_le 0 0); omega. compute; auto. } rewrite <- (Int64.unsigned_repr n') by (unfold Int64.max_unsigned; omega). @@ -1306,7 +1306,7 @@ Proof. assert (Int64.min_signed <= n'). { rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply (int_round_odd_le 0 0); omega. } assert (n' <= Int64.max_signed). - { apply Zle_trans with (int_round_odd Int64.max_signed 11). + { apply Z.le_trans with (int_round_odd Int64.max_signed 11). rewrite <- H1. apply (int_round_odd_le 0 0); omega. compute; intuition congruence. } rewrite <- (Int64.signed_repr n') by omega. @@ -1321,7 +1321,7 @@ Proof. change (Int64.unsigned (Int64.repr 2047)) with 2047. change 2047 with (Z.ones 11). rewrite ! Z.land_ones by omega. rewrite Int64.unsigned_repr. apply Int64.eqmod_mod_eq. - apply Zlt_gt. apply (Zpower_gt_0 radix2); omega. + apply Z.lt_gt. apply (Zpower_gt_0 radix2); omega. apply Int64.eqmod_divides with (2^64). apply Int64.eqm_signed_unsigned. exists (2^(64-11)); auto. exploit (Z_mod_lt (Int64.unsigned n) (2^11)). compute; auto. |