14 lines
629 B
Diff
14 lines
629 B
Diff
--- ./lib/coq/WhyFloats.v.orig 2014-03-17 16:01:46.000000000 -0600
|
|
+++ ./lib/coq/WhyFloats.v 2014-09-02 17:40:03.356028320 -0600
|
|
@@ -106,9 +106,9 @@ apply Zlt_succ_le.
|
|
change (Zpos m < Zsucc (Zpred (Zpower_pos 2 prec)))%Z.
|
|
rewrite <- Zsucc_pred.
|
|
generalize (Zeq_bool_eq _ _ H1). clear.
|
|
-rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
|
|
+rewrite Fcore_digits.Zpos_digits2_pos.
|
|
intros H.
|
|
-apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
|
|
+apply (Fcore_digits.Zpower_gt_Zdigits Fcore_Zaux.radix2 (Zpos prec) (Zpos m)).
|
|
revert H.
|
|
unfold FLT_exp.
|
|
generalize (Fcore_digits.Zdigits radix2 (Zpos m)).
|