From fad5113b1216ce735565c44b3bb2a21b76d692aa Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 14 Sep 2018 12:15:01 +0000 Subject: 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. --- flocq/Appli/Fappli_IEEE.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'flocq') 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 : -- cgit