diff options
| -rw-r--r-- | flocq/Appli/Fappli_IEEE.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v index 161b545a..7503dc1d 100644 --- a/flocq/Appli/Fappli_IEEE.v +++ b/flocq/Appli/Fappli_IEEE.v @@ -597,9 +597,8 @@ revert H1. clear -H2. rewrite Zpos_digits2_pos. unfold fexp, FLT_exp. generalize (Zdigits radix2 (Zpos mx)). -intros ; zify ; subst. -clear -H H2. clearbody emin. -omega. +clearbody emin. +intros ; zify ; omega. Qed. Theorem abs_B2R_lt_emax : |