diff options
| author | Vincent Laporte <vbgl@users.noreply.github.com> | 2018-09-14 12:15:01 +0000 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-09-14 14:15:01 +0200 |
| commit | fad5113b1216ce735565c44b3bb2a21b76d692aa (patch) | |
| tree | 90d44e1cb8a153eba1ea2592613163ed159be6b0 /flocq | |
| parent | 932d40637eaa84e6d335a0a997eacc35379e2bec (diff) | |
| download | compcert-kvx-fad5113b1216ce735565c44b3bb2a21b76d692aa.tar.gz compcert-kvx-fad5113b1216ce735565c44b3bb2a21b76d692aa.zip | |
flocq: minor cleaning (#257)
This change avoids relying on generated names, making the proof script compatible with ongoing evolutions of the `zify` tactic.
A similar cleanup was already performed in Flocq's master sources.
Diffstat (limited to 'flocq')
| -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 : |