Commit dc130db8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Ensure compatibility with Coq 8.5.

parent d972973c
......@@ -646,8 +646,9 @@ case Zlt_bool_spec ; intros Hk.
(* *)
unfold truncate_aux.
rewrite Fx at 1.
refine (let H := _ in conj _ H).
assert (H: (e + k)%Z = canonic_exp beta fexp x).
unfold k. ring.
refine (conj _ H).
rewrite <- H.
apply F2R_eq_compat.
replace (scaled_mantissa beta fexp x) with (Z2R (Zfloor (scaled_mantissa beta fexp x))).
......
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