diff options
Diffstat (limited to 'theories/Floats')
| -rw-r--r-- | theories/Floats/FloatLemmas.v | 2 | ||||
| -rw-r--r-- | theories/Floats/FloatOps.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/Floats/FloatLemmas.v b/theories/Floats/FloatLemmas.v index 81cb7120e0..5db501742f 100644 --- a/theories/Floats/FloatLemmas.v +++ b/theories/Floats/FloatLemmas.v @@ -24,7 +24,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S destruct (Prim2SF f); auto. unfold SFldexp. unfold binary_round. - assert (Hmod_elim : forall e, ([| of_Z (Z.max (Z.min e (emax - emin)) (emin - emax - 1) + shift)|]%int63 - shift = Z.max (Z.min e (emax - emin)) (emin - emax - 1))%Z). + assert (Hmod_elim : forall e, (φ (of_Z (Z.max (Z.min e (emax - emin)) (emin - emax - 1) + shift))%int63 - shift = Z.max (Z.min e (emax - emin)) (emin - emax - 1))%Z). { intro e1. rewrite of_Z_spec, shift_value. diff --git a/theories/Floats/FloatOps.v b/theories/Floats/FloatOps.v index f0d3bcced9..e74cb09c27 100644 --- a/theories/Floats/FloatOps.v +++ b/theories/Floats/FloatOps.v @@ -10,7 +10,7 @@ Definition shift := 2101%Z. (** [= 2*emax + prec] *) Definition frexp f := let (m, se) := frshiftexp f in - (m, ([| se |] - shift)%Z%int63). + (m, (φ se - shift)%Z%int63). Definition ldexp f e := let e' := Z.max (Z.min e (emax - emin)) (emin - emax - 1) in @@ -28,7 +28,7 @@ Definition Prim2SF f := else let (r, exp) := frexp f in let e := (exp - prec)%Z in - let (shr, e') := shr_fexp prec emax [| normfr_mantissa r |]%int63 e loc_Exact in + let (shr, e') := shr_fexp prec emax (φ (normfr_mantissa r))%int63 e loc_Exact in match shr_m shr with | Zpos p => S754_finite (get_sign f) p e' | Zneg _ | Z0 => S754_zero false (* must never occur *) |