Commit 6236657f authored by Guillaume Melquiond's avatar Guillaume Melquiond

Ensure compatibility with Flocq 2.5.

parent 2f56d736
...@@ -552,13 +552,13 @@ if test "$enable_coq_libs" = yes; then ...@@ -552,13 +552,13 @@ if test "$enable_coq_libs" = yes; then
AC_MSG_CHECKING([for Flocq]) AC_MSG_CHECKING([for Flocq])
AS_IF( AS_IF(
[ echo "Require Import Flocq.Flocq_version BinNat." \ [ echo "Require Import Flocq.Flocq_version BinNat." \
"Goal (20200 <= Flocq_version)%N. easy. Qed." > conftest.v "Goal (20500 <= Flocq_version)%N. easy. Qed." > conftest.v
"$COQC" conftest.v > conftest.err ], "$COQC" conftest.v > conftest.err ],
[ AC_MSG_RESULT(yes) ], [ AC_MSG_RESULT(yes) ],
[ AC_MSG_RESULT(no) [ AC_MSG_RESULT(no)
enable_coq_fp_libs=no enable_coq_fp_libs=no
AC_MSG_WARN(Cannot find Flocq.) AC_MSG_WARN(Cannot find Flocq.)
reason_coq_fp_libs=" (Flocq >= 2.2 not found)" ]) reason_coq_fp_libs=" (Flocq >= 2.5 not found)" ])
rm -f conftest.v conftest.vo conftest.err rm -f conftest.v conftest.vo conftest.err
fi fi
......
...@@ -305,9 +305,9 @@ apply generic_format_B2R. ...@@ -305,9 +305,9 @@ apply generic_format_B2R.
apply generic_format_bpow. apply generic_format_bpow.
unfold FLT_exp, emin. unfold FLT_exp, emin.
zify ; generalize Hprec' Hemax' ; omega. zify ; generalize Hprec' Hemax' ; omega.
apply bpow_gt_0.
apply abs_B2R_lt_emax. apply abs_B2R_lt_emax.
unfold pred. rewrite pred_eq_pos.
unfold pred_pos.
rewrite ln_beta_bpow. rewrite ln_beta_bpow.
ring_simplify (emax+1-1)%Z. ring_simplify (emax+1-1)%Z.
rewrite Req_bool_true by easy. rewrite Req_bool_true by easy.
...@@ -322,6 +322,7 @@ simpl; ring. ...@@ -322,6 +322,7 @@ simpl; ring.
apply Zlt_le_weak. apply Zlt_le_weak.
exact Hprec'. exact Hprec'.
generalize Hprec' Hemax' ; omega. generalize Hprec' Hemax' ; omega.
apply bpow_ge_0.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
......
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