Commit 50656d81 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove some obsolete Coq notations.

Since these files depend on Flocq, we are sure that Coq is at least 8.7.
parent 3895e560
......@@ -72,7 +72,7 @@ apply Rmult_le_compat.
now apply (IZR_le 0).
apply bpow_ge_0.
apply IZR_le.
apply (Z.lt_le_pred (Zabs (Zpos m)) (Zpower radix2 24)).
apply (Z.lt_le_pred (Z.abs (Zpos m)) (Zpower radix2 24)).
apply Digits.Zpower_gt_Zdigits.
revert H1.
generalize (Digits.Zdigits radix2 (Z.pos m)).
......
......@@ -74,7 +74,7 @@ apply Rmult_le_compat.
now apply (IZR_le 0).
apply bpow_ge_0.
apply IZR_le.
apply (Z.lt_le_pred (Zabs (Zpos m)) (Zpower radix2 53)).
apply (Z.lt_le_pred (Z.abs (Zpos m)) (Zpower radix2 53)).
apply Digits.Zpower_gt_Zdigits.
revert H1.
generalize (Digits.Zdigits radix2 (Z.pos m)).
......
......@@ -1207,7 +1207,7 @@ Proof.
fold sb.
unfold FLT_exp.
replace (sb - 1 + 1 + 1 - sb)%Z with 1%Z by ring.
apply Zmax_l.
apply Z.max_l.
pose sb_gt_1; pose Hemax'; omega.
apply Zle_bool_true.
pose Hemax'; pose Hsbb; omega.
......@@ -1276,7 +1276,7 @@ Lemma Exact_rounding_for_integers :
Proof with auto with typeclass_instances.
intros m z Hz.
apply round_generic...
assert (Zabs z <= pow2sb)%Z.
assert (Z.abs z <= pow2sb)%Z.
apply Z.abs_le with (1:=Hz).
destruct (Zle_lt_or_eq _ _ H) as [Bz|Bz] ; clear H Hz.
apply generic_format_FLT.
......@@ -4633,7 +4633,7 @@ Proof.
fold sb.
unfold FLT_exp.
replace (sb - 1 + 1 + - sb)%Z with 0%Z by ring.
apply Zmax_l.
apply Z.max_l.
pose sb_gt_1; pose Hemax'; omega.
apply Zle_bool_true.
pose Hemax'; pose sb_gt_1; omega.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment