Consolidate int63-related notations

We avoid redundant notations for the same concepts and make sure
notations do not break Ltac parsing for users of these libraries.

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 *)