Upgrade embedded version of Flocq to 3.1.

Main changes to CompCert outside of Flocq are as follows:

- Minimal supported version of Coq is now 8.7, due to Flocq requirements.

- Most modifications are due to Z2R being dropped in favor of IZR and to
  the way Flocq now handles NaNs.

- CompCert now correctly handles NaNs for the Risc-V architecture
  (hopefully).

2 files changed, 371 insertions, 366 deletions

diff --git a/lib/Fappli_IEEE_extra.v b/lib/Fappli_IEEE_extra.v
index 85fadc16..c23149be 100644
--- a/lib/Fappli_IEEE_extra.v
+++ b/lib/Fappli_IEEE_extra.v
@@ -20,15 +20,8 @@
 Require Import Psatz.
 Require Import Bool.
 Require Import Eqdep_dec.
-Require Import Fcore.
-Require Import Fcore_digits.
-Require Import Fcalc_digits.
-Require Import Fcalc_ops.
-Require Import Fcalc_round.
-Require Import Fcalc_bracket.
-Require Import Fprop_Sterbenz.
-Require Import Fappli_IEEE.
-Require Import Fappli_rnd_odd.
+(*From Flocq *)
+Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd.
 
 Local Open Scope Z_scope.
 
@@ -65,7 +58,7 @@ Definition is_finite_pos0 (f: binary_float) : bool :=
   match f with
   | B754_zero _ _ s => negb s
   | B754_infinity _ _ _ => false
-  | B754_nan _ _ _ _ => false
+  | B754_nan _ _ _ _ _ => false
   | B754_finite _ _ _ _ _ _ => true
   end.
 
@@ -74,10 +67,10 @@ Lemma Bsign_pos0:
 Proof.
   intros. destruct x as [ [] | | | [] ex mx Bx ]; try discriminate; simpl.
 - rewrite Rlt_bool_false; auto. lra.
-- rewrite Rlt_bool_true; auto. apply F2R_lt_0_compat. compute; auto.
+- rewrite Rlt_bool_true; auto. apply F2R_lt_0. compute; auto.
 - rewrite Rlt_bool_false; auto.
   assert ((F2R (Float radix2 (Z.pos ex) mx) > 0)%R) by
-    ( apply F2R_gt_0_compat; compute; auto ).
+    ( apply F2R_gt_0; compute; auto ).
   lra.
 Qed.
 
@@ -101,18 +94,18 @@ Proof.
   assert (UIP_bool: forall (b1 b2: bool) (e e': b1 = b2), e = e').
   { intros. apply UIP_dec. decide equality. }
   Ltac try_not_eq := try solve [right; congruence].
-  destruct f1 as [| |? []|], f2 as [| |? []|];
-  try destruct b; try destruct b0;
+  destruct f1 as [s1|s1|s1 p1 H1|s1 m1 e1 H1], f2 as [s2|s2|s2 p2 H2|s2 m2 e2 H2];
+  try destruct s1; try destruct s2;
   try solve [left; auto]; try_not_eq.
-  destruct (Pos.eq_dec x x0); try_not_eq;
+  destruct (Pos.eq_dec p1 p2); try_not_eq;
     subst; left; f_equal; f_equal; apply UIP_bool.
-  destruct (Pos.eq_dec x x0); try_not_eq;
+  destruct (Pos.eq_dec p1 p2); try_not_eq;
     subst; left; f_equal; f_equal; apply UIP_bool.
-  destruct (Pos.eq_dec m m0); try_not_eq;
-  destruct (Z.eq_dec e e1); try solve [right; intro H; inversion H; congruence];
+  destruct (Pos.eq_dec m1 m2); try_not_eq;
+  destruct (Z.eq_dec e1 e2); try solve [right; intro H; inversion H; congruence];
   subst; left; f_equal; apply UIP_bool.
-  destruct (Pos.eq_dec m m0); try_not_eq;
-  destruct (Z.eq_dec e e1); try solve [right; intro H; inversion H; congruence];
+  destruct (Pos.eq_dec m1 m2); try_not_eq;
+  destruct (Z.eq_dec e1 e2); try solve [right; intro H; inversion H; congruence];
   subst; left; f_equal; apply UIP_bool.
 Defined.
 
@@ -121,7 +114,7 @@ Defined.
 (** Integers that can be represented exactly as FP numbers. *)
 
 Definition integer_representable (n: Z): Prop :=
-  Z.abs n <= 2^emax - 2^(emax - prec) /\ generic_format radix2 fexp (Z2R n).
+  Z.abs n <= 2^emax - 2^(emax - prec) /\ generic_format radix2 fexp (IZR n).
 
 Let int_upper_bound_eq: 2^emax - 2^(emax - prec) = (2^prec - 1) * 2^(emax - prec).
 Proof.
@@ -142,9 +135,9 @@ Proof.
   rewrite Z.abs_mul. f_equal. rewrite Z.abs_eq. auto. apply (Zpower_ge_0 radix2).
 - apply generic_format_FLT. exists (Float radix2 n p).
   unfold F2R; simpl.
-  split. rewrite <- Z2R_Zpower by auto. apply Z2R_mult.
-  split. zify; omega.
-  unfold emin; red in prec_gt_0_; omega.
+  rewrite <- IZR_Zpower by auto. apply mult_IZR.
+  simpl; zify; omega.
+  unfold emin, Fexp; red in prec_gt_0_; omega.
 Qed.
 
 Lemma integer_representable_2p:
@@ -166,16 +159,16 @@ Proof.
 - red in prec_gt_0_.
   apply generic_format_FLT. exists (Float radix2 1 p).
   unfold F2R; simpl.
-  split. rewrite Rmult_1_l. rewrite <- Z2R_Zpower. auto. omega.
-  split. change 1 with (2^0). apply (Zpower_lt radix2). omega. auto.
-  unfold emin; omega.
+  rewrite Rmult_1_l. rewrite <- IZR_Zpower. auto. omega.
+  simpl Z.abs. change 1 with (2^0). apply (Zpower_lt radix2). omega. auto.
+  unfold emin, Fexp; omega.
 Qed.
 
 Lemma integer_representable_opp:
   forall n, integer_representable n -> integer_representable (-n).
 Proof.
   intros n (A & B); split. rewrite Z.abs_opp. auto.
-  rewrite Z2R_opp. apply generic_format_opp; auto.
+  rewrite opp_IZR. apply generic_format_opp; auto.
 Qed.
 
 Lemma integer_representable_n2p_wide:
@@ -204,19 +197,20 @@ Qed.
 Lemma round_int_no_overflow:
   forall n,
   Z.abs n <= 2^emax - 2^(emax-prec) ->
-  (Rabs (round radix2 fexp (round_mode mode_NE) (Z2R n)) < bpow radix2 emax)%R.
+  (Rabs (round radix2 fexp (round_mode mode_NE) (IZR n)) < bpow radix2 emax)%R.
 Proof.
   intros. red in prec_gt_0_.
   rewrite <- round_NE_abs.
-  apply Rle_lt_trans with (Z2R (2^emax - 2^(emax-prec))).
+  apply Rle_lt_trans with (IZR (2^emax - 2^(emax-prec))).
   apply round_le_generic. apply fexp_correct; auto. apply valid_rnd_N.
   apply generic_format_FLT. exists (Float radix2 (2^prec-1) (emax-prec)).
   rewrite int_upper_bound_eq. unfold F2R; simpl.
-  split. rewrite <- Z2R_Zpower by omega. rewrite <- Z2R_mult. auto.
-  split. assert (0 < 2^prec) by (apply (Zpower_gt_0 radix2); omega). zify; omega.
-  unfold emin; omega.
-  rewrite <- Z2R_abs. apply Z2R_le. auto.
-  rewrite <- Z2R_Zpower by omega. apply Z2R_lt. simpl.
+  rewrite <- IZR_Zpower by omega. rewrite <- mult_IZR. auto.
+  assert (0 < 2^prec) by (apply (Zpower_gt_0 radix2); omega).
+  unfold Fnum; simpl; zify; omega.
+  unfold emin, Fexp; omega.
+  rewrite <- abs_IZR. apply IZR_le. auto.
+  rewrite <- IZR_Zpower by omega. apply IZR_lt. simpl.
   assert (0 < 2^(emax-prec)) by (apply (Zpower_gt_0 radix2); omega).
   omega.
   apply fexp_correct. auto.
@@ -229,9 +223,9 @@ Definition BofZ (n: Z) : binary_float :=
 
 Theorem BofZ_correct:
   forall n,
-  if Rlt_bool (Rabs (round radix2 fexp (round_mode mode_NE) (Z2R n))) (bpow radix2 emax)
+  if Rlt_bool (Rabs (round radix2 fexp (round_mode mode_NE) (IZR n))) (bpow radix2 emax)
   then
-    B2R prec emax (BofZ n) = round radix2 fexp (round_mode mode_NE) (Z2R n) /\
+    B2R prec emax (BofZ n) = round radix2 fexp (round_mode mode_NE) (IZR n) /\
     is_finite _ _ (BofZ n) = true /\
     Bsign prec emax (BofZ n) = Z.ltb n 0
   else
@@ -240,24 +234,24 @@ Proof.
   intros.
   generalize (binary_normalize_correct prec emax prec_gt_0_ Hmax mode_NE n 0 false).
   fold emin; fold fexp; fold (BofZ n).
-  replace (F2R {| Fnum := n; Fexp := 0 |}) with (Z2R n).
+  replace (F2R {| Fnum := n; Fexp := 0 |}) with (IZR n).
   destruct Rlt_bool.
 - intros (A & B & C). split; [|split].
   + auto.
   + auto.
-  + rewrite C. change 0%R with (Z2R 0). rewrite Rcompare_Z2R.
+  + rewrite C. rewrite Rcompare_IZR.
     unfold Z.ltb. auto.
-- intros A; rewrite A. f_equal. change 0%R with (Z2R 0).
+- intros A; rewrite A. f_equal.
   generalize (Z.ltb_spec n 0); intros SPEC; inversion SPEC.
-  apply Rlt_bool_true; apply Z2R_lt; auto.
-  apply Rlt_bool_false; apply Z2R_le; auto.
+  apply Rlt_bool_true; apply IZR_lt; auto.
+  apply Rlt_bool_false; apply IZR_le; auto.
 - unfold F2R; simpl. ring.
 Qed.
 
 Theorem BofZ_finite:
   forall n,
   Z.abs n <= 2^emax - 2^(emax-prec) ->
-  B2R _ _ (BofZ n) = round radix2 fexp (round_mode mode_NE) (Z2R n)
+  B2R _ _ (BofZ n) = round radix2 fexp (round_mode mode_NE) (IZR n)
   /\ is_finite _ _ (BofZ n) = true
   /\ Bsign _ _ (BofZ n) = Z.ltb n 0%Z.
 Proof.
@@ -269,7 +263,7 @@ Qed.
 Theorem BofZ_representable:
   forall n,
   integer_representable n ->
-  B2R _ _ (BofZ n) = Z2R n
+  B2R _ _ (BofZ n) = IZR n
   /\ is_finite _ _ (BofZ n) = true
   /\ Bsign _ _ (BofZ n) = (n <? 0).
 Proof.
@@ -280,7 +274,7 @@ Qed.
 Theorem BofZ_exact:
   forall n,
   -2^prec <= n <= 2^prec ->
-  B2R _ _ (BofZ n) = Z2R n
+  B2R _ _ (BofZ n) = IZR n
   /\ is_finite _ _ (BofZ n) = true
   /\ Bsign _ _ (BofZ n) = Z.ltb n 0%Z.
 Proof.
@@ -294,20 +288,19 @@ Proof.
   intros.
   generalize (binary_normalize_correct prec emax prec_gt_0_ Hmax mode_NE n 0 false).
   fold emin; fold fexp; fold (BofZ n).
-  replace (F2R {| Fnum := n; Fexp := 0 |}) with (Z2R n) by
+  replace (F2R {| Fnum := n; Fexp := 0 |}) with (IZR n) by
     (unfold F2R; simpl; ring).
   rewrite Rlt_bool_true by (apply round_int_no_overflow; auto).
   intros (A & B & C).
   destruct (BofZ n); auto; try discriminate.
-  simpl in *. rewrite C. change 0%R with (Z2R 0). rewrite Rcompare_Z2R.
+  simpl in *. rewrite C. rewrite Rcompare_IZR.
   generalize (Zcompare_spec n 0); intros SPEC; inversion SPEC; auto.
-  assert ((round radix2 fexp ZnearestE (Z2R n) <= -1)%R).
-  { change (-1)%R with (Z2R (-1)).
-    apply round_le_generic. apply fexp_correct. auto. apply valid_rnd_N.
+  assert ((round radix2 fexp ZnearestE (IZR n) <= -1)%R).
+  { apply round_le_generic. apply fexp_correct. auto. apply valid_rnd_N.
     apply (integer_representable_opp 1).
     apply (integer_representable_2p 0).
     red in prec_gt_0_; omega.
-    apply Z2R_le; omega.
+    apply IZR_le; omega.
   }
   lra.
 Qed.
@@ -334,13 +327,13 @@ Proof.
   destruct (BofZ_representable q) as (D & E & F); auto.
   generalize (Bplus_correct _ _ _ Hmax nan mode_NE (BofZ p) (BofZ q) B E).
   fold emin; fold fexp.
-  rewrite A, D. rewrite <- Z2R_plus.
+  rewrite A, D. rewrite <- plus_IZR.
   generalize (BofZ_correct (p + q)). destruct Rlt_bool.
 - intros (P & Q & R) (U & V & W).
   apply B2R_Bsign_inj; auto.
   rewrite P, U; auto.
   rewrite R, W, C, F.
-  change 0%R with (Z2R 0). rewrite Rcompare_Z2R. unfold Z.ltb at 3.
+  rewrite Rcompare_IZR. unfold Z.ltb at 3.
   generalize (Zcompare_spec (p + q) 0); intros SPEC; inversion SPEC; auto.
   assert (EITHER: 0 <= p \/ 0 <= q) by omega.
   destruct EITHER; [apply andb_false_intro1 | apply andb_false_intro2];
@@ -364,13 +357,13 @@ Proof.
   destruct (BofZ_representable q) as (D & E & F); auto.
   generalize (Bminus_correct _ _ _ Hmax nan mode_NE (BofZ p) (BofZ q) B E).
   fold emin; fold fexp.
-  rewrite A, D. rewrite <- Z2R_minus.
+  rewrite A, D. rewrite <- minus_IZR.
   generalize (BofZ_correct (p - q)). destruct Rlt_bool.
 - intros (P & Q & R) (U & V & W).
   apply B2R_Bsign_inj; auto.
   rewrite P, U; auto.
   rewrite R, W, C, F.
-  change 0%R with (Z2R 0). rewrite Rcompare_Z2R. unfold Z.ltb at 3.
+  rewrite Rcompare_IZR. unfold Z.ltb at 3.
   generalize (Zcompare_spec (p - q) 0); intros SPEC; inversion SPEC; auto.
   assert (EITHER: 0 <= p \/ q < 0) by omega.
   destruct EITHER; [apply andb_false_intro1 | apply andb_false_intro2].
@@ -405,7 +398,7 @@ Proof.
   destruct (BofZ_representable q) as (D & E & F); auto.
   generalize (Bmult_correct _ _ _ Hmax nan mode_NE (BofZ p) (BofZ q)).
   fold emin; fold fexp.
-  rewrite A, B, C, D, E, F. rewrite <- Z2R_mult.
+  rewrite A, B, C, D, E, F. rewrite <- mult_IZR.
   generalize (BofZ_correct (p * q)). destruct Rlt_bool.
 - intros (P & Q & R) (U & V & W).
   apply B2R_Bsign_inj; auto.
@@ -431,36 +424,36 @@ Proof.
     apply integer_representable_2p. auto.
     apply (Zpower_gt_0 radix2).
     omega.
-- assert (Z2R x <> 0%R) by (apply (Z2R_neq _ _ n)).
+- assert (IZR x <> 0%R) by (apply (IZR_neq _ _ n)).
   destruct (BofZ_finite x H) as (A & B & C).
   destruct (BofZ_representable (2^p)) as (D & E & F).
     apply integer_representable_2p. auto.
-  assert (canonic_exp radix2 fexp (Z2R (x * 2^p)) =
-          canonic_exp radix2 fexp (Z2R x) + p).
+  assert (cexp radix2 fexp (IZR (x * 2^p)) =
+          cexp radix2 fexp (IZR x) + p).
   {
-    unfold canonic_exp, fexp. rewrite Z2R_mult.
-    change (2^p) with (radix2^p). rewrite Z2R_Zpower by omega.
-    rewrite ln_beta_mult_bpow by auto.
-    assert (prec + 1 <= ln_beta radix2 (Z2R x)).
-    { rewrite <- (ln_beta_abs radix2 (Z2R x)).
-      rewrite <- (ln_beta_bpow radix2 prec).
-      apply ln_beta_le.
-      apply bpow_gt_0. rewrite <- Z2R_Zpower by (red in prec_gt_0_;omega).
-      rewrite <- Z2R_abs. apply Z2R_le; auto. }
+    unfold cexp, fexp. rewrite mult_IZR.
+    change (2^p) with (radix2^p). rewrite IZR_Zpower by omega.
+    rewrite mag_mult_bpow by auto.
+    assert (prec + 1 <= mag radix2 (IZR x)).
+    { rewrite <- (mag_abs radix2 (IZR x)).
+      rewrite <- (mag_bpow radix2 prec).
+      apply mag_le.
+      apply bpow_gt_0. rewrite <- IZR_Zpower by (red in prec_gt_0_;omega).
+      rewrite <- abs_IZR. apply IZR_le; auto. }
     unfold FLT_exp.
     unfold emin; red in prec_gt_0_; zify; omega.
   }
-  assert (forall m, round radix2 fexp m (Z2R x) * Z2R (2^p) =
-                    round radix2 fexp m (Z2R (x * 2^p)))%R.
+  assert (forall m, round radix2 fexp m (IZR x) * IZR (2^p) =
+                    round radix2 fexp m (IZR (x * 2^p)))%R.
   {
     intros. unfold round, scaled_mantissa. rewrite H3.
-    rewrite Z2R_mult. rewrite Z.opp_add_distr. rewrite bpow_plus.
-    set (a := Z2R x); set (b := bpow radix2 (- canonic_exp radix2 fexp a)).
-    replace (a * Z2R (2^p) * (b * bpow radix2 (-p)))%R with (a * b)%R.
+    rewrite mult_IZR. rewrite Z.opp_add_distr. rewrite bpow_plus.
+    set (a := IZR x); set (b := bpow radix2 (- cexp radix2 fexp a)).
+    replace (a * IZR (2^p) * (b * bpow radix2 (-p)))%R with (a * b)%R.
     unfold F2R; simpl. rewrite Rmult_assoc. f_equal.
-    rewrite bpow_plus.  f_equal. apply (Z2R_Zpower radix2). omega.
-    transitivity ((a * b) * (Z2R (2^p) * bpow radix2 (-p)))%R.
-    rewrite (Z2R_Zpower radix2). rewrite <- bpow_plus.
+    rewrite bpow_plus.  f_equal. apply (IZR_Zpower radix2). omega.
+    transitivity ((a * b) * (IZR (2^p) * bpow radix2 (-p)))%R.
+    rewrite (IZR_Zpower radix2). rewrite <- bpow_plus.
     replace (p + -p) with 0 by omega. change (bpow radix2 0) with 1%R. ring.
     omega.
     ring.
@@ -502,7 +495,7 @@ Lemma round_odd_flt:
   round radix2 fexp (Znearest choice) (round radix2 (FLT_exp emin' prec') Zrnd_odd x) =
   round radix2 fexp (Znearest choice) x.
 Proof.
-  intros. apply round_odd_prop. auto. apply fexp_correct; auto.
+  intros. apply round_N_odd. auto. apply fexp_correct; auto.
   apply exists_NE_FLT. right; omega.
   apply FLT_exp_valid. red; omega.
   apply exists_NE_FLT. right; omega.
@@ -519,17 +512,17 @@ Corollary round_odd_fix:
 Proof.
   intros. destruct (Req_EM_T x 0%R).
 - subst x. rewrite round_0. auto. apply valid_rnd_odd.
-- set (prec' := ln_beta radix2 x - p).
+- set (prec' := mag radix2 x - p).
   set (emin' := emin - 2).
-  assert (PREC: ln_beta radix2 (bpow radix2 (prec + p + 1)) <= ln_beta radix2 x).
-  { rewrite <- (ln_beta_abs radix2 x).
-    apply ln_beta_le; auto. apply bpow_gt_0. }
-  rewrite ln_beta_bpow in PREC.
-  assert (CANON: canonic_exp radix2 (FLT_exp emin' prec') x =
-                 canonic_exp radix2 (FIX_exp p) x).
+  assert (PREC: mag radix2 (bpow radix2 (prec + p + 1)) <= mag radix2 x).
+  { rewrite <- (mag_abs radix2 x).
+    apply mag_le; auto. apply bpow_gt_0. }
+  rewrite mag_bpow in PREC.
+  assert (CANON: cexp radix2 (FLT_exp emin' prec') x =
+                 cexp radix2 (FIX_exp p) x).
   {
-    unfold canonic_exp, FLT_exp, FIX_exp.
-    replace (ln_beta radix2 x - prec') with p by (unfold prec'; omega).
+    unfold cexp, FLT_exp, FIX_exp.
+    replace (mag radix2 x - prec') with p by (unfold prec'; omega).
     apply Z.max_l. unfold emin', emin. red in prec_gt_0_; omega.
   }
   assert (RND: round radix2 (FIX_exp p) Zrnd_odd x =
@@ -549,7 +542,7 @@ Definition int_round_odd (x: Z) (p: Z) :=
 
 Lemma Zrnd_odd_int:
   forall n p, 0 <= p ->
-  Zrnd_odd (Z2R n * bpow radix2 (-p)) * 2^p =
+  Zrnd_odd (IZR n * bpow radix2 (-p)) * 2^p =
   int_round_odd n p.
 Proof.
   intros.
@@ -561,29 +554,29 @@ Proof.
   pose proof (bpow_gt_0 radix2 (-p)).
   assert (bpow radix2 p * bpow radix2 (-p) = 1)%R.
   { rewrite <- bpow_plus. replace (p + -p) with 0 by omega. auto. }
-  assert (Z2R n * bpow radix2 (-p) = Z2R q + Z2R r * bpow radix2 (-p))%R.
-  { rewrite H1. rewrite Z2R_plus, Z2R_mult.
-    change (Z2R (2^p)) with (Z2R (radix2^p)).
-    rewrite Z2R_Zpower by omega. ring_simplify.
+  assert (IZR n * bpow radix2 (-p) = IZR q + IZR r * bpow radix2 (-p))%R.
+  { rewrite H1. rewrite plus_IZR, mult_IZR.
+    change (IZR (2^p)) with (IZR (radix2^p)).
+    rewrite IZR_Zpower by omega. ring_simplify.
     rewrite Rmult_assoc. rewrite H4. ring. }
-  assert (0 <= Z2R r < bpow radix2 p)%R.
-  { split. change 0%R with (Z2R 0). apply Z2R_le; omega.
-    rewrite <- Z2R_Zpower by omega. apply Z2R_lt; tauto. }
-  assert (0 <= Z2R r * bpow radix2 (-p) < 1)%R.
+  assert (0 <= IZR r < bpow radix2 p)%R.
+  { split. apply IZR_le; omega.
+    rewrite <- IZR_Zpower by omega. apply IZR_lt; tauto. }
+  assert (0 <= IZR r * bpow radix2 (-p) < 1)%R.
   { generalize (bpow_gt_0 radix2 (-p)). intros.
     split. apply Rmult_le_pos; lra.
     rewrite <- H4. apply Rmult_lt_compat_r. auto. tauto. }
-  assert (Zfloor (Z2R n * bpow radix2 (-p)) = q).
-  { apply Zfloor_imp. rewrite H5. rewrite Z2R_plus. change (Z2R 1) with 1%R. lra. }
+  assert (Zfloor (IZR n * bpow radix2 (-p)) = q).
+  { apply Zfloor_imp. rewrite H5. rewrite plus_IZR. lra. }
   unfold Zrnd_odd. destruct Req_EM_T.
-- assert (Z2R r * bpow radix2 (-p) = 0)%R.
+- assert (IZR r * bpow radix2 (-p) = 0)%R.
   { rewrite H8 in e. rewrite e in H5. lra. }
   apply Rmult_integral in H9. destruct H9; [ | lra ].
-  apply (eq_Z2R r 0) in H9. apply <- Z.eqb_eq in H9. rewrite H9. assumption.
-- assert (Z2R r * bpow radix2 (-p) <> 0)%R.
+  apply (eq_IZR r 0) in H9. apply <- Z.eqb_eq in H9. rewrite H9. assumption.
+- assert (IZR r * bpow radix2 (-p) <> 0)%R.
   { rewrite H8 in n0. lra. }
   destruct (Z.eqb r 0) eqn:RZ.
-  apply Z.eqb_eq in RZ. rewrite RZ in H9. change (Z2R 0) with 0%R in H9.
+  apply Z.eqb_eq in RZ. rewrite RZ in H9.
   rewrite Rmult_0_l in H9. congruence.
   rewrite Zceil_floor_neq by lra. rewrite H8.
   change Zeven with Z.even. rewrite Zodd_even_bool. destruct (Z.even q); auto.
@@ -594,9 +587,9 @@ Lemma int_round_odd_le:
   x <= y -> int_round_odd x p <= int_round_odd y p.
 Proof.
   intros.
-  assert (Zrnd_odd (Z2R x * bpow radix2 (-p)) <= Zrnd_odd (Z2R y * bpow radix2 (-p))).
+  assert (Zrnd_odd (IZR x * bpow radix2 (-p)) <= Zrnd_odd (IZR y * bpow radix2 (-p))).
   { apply Zrnd_le. apply valid_rnd_odd. apply Rmult_le_compat_r. apply bpow_ge_0.
-    apply Z2R_le; auto. }
+    apply IZR_le; auto. }
   rewrite <- ! Zrnd_odd_int by auto.
   apply Zmult_le_compat_r. auto. apply (Zpower_ge_0 radix2).
 Qed.
@@ -635,14 +628,14 @@ Proof.
   destruct (BofZ_finite (int_round_odd x p) YRANGE) as (Y1 & Y2 & Y3).
   apply BofZ_finite_equal; auto.
   rewrite X1, Y1.
-  assert (Z2R (int_round_odd x p) = round radix2 (FIX_exp p) Zrnd_odd (Z2R x)).
+  assert (IZR (int_round_odd x p) = round radix2 (FIX_exp p) Zrnd_odd (IZR x)).
   {
-     unfold round, scaled_mantissa, canonic_exp, FIX_exp.
+     unfold round, scaled_mantissa, cexp, FIX_exp.
      rewrite <- Zrnd_odd_int by omega.
-     unfold F2R; simpl. rewrite Z2R_mult. f_equal. apply (Z2R_Zpower radix2). omega.
+     unfold F2R; simpl. rewrite mult_IZR. f_equal. apply (IZR_Zpower radix2). omega.
   }
   rewrite H. symmetry. apply round_odd_fix. auto. omega.
-  rewrite <- Z2R_Zpower. rewrite <- Z2R_abs. apply Z2R_le; auto.
+  rewrite <- IZR_Zpower. rewrite <- abs_IZR. apply IZR_le; auto.
   red in prec_gt_0_; omega.
 Qed.
 
@@ -704,37 +697,37 @@ Theorem ZofB_correct:
   forall f,
   ZofB f = if is_finite _ _ f then Some (Ztrunc (B2R _ _ f)) else None.
 Proof.
-  destruct f; simpl; auto.
-- f_equal. symmetry. apply (Ztrunc_Z2R 0).
+  destruct f as [s|s|s p H|s m e H]; simpl; auto.
+- f_equal. symmetry. apply (Ztrunc_IZR 0).
 - destruct e; f_equal.
-  + unfold F2R; simpl. rewrite Rmult_1_r. rewrite Ztrunc_Z2R. auto.
-  + unfold F2R; simpl. rewrite <- Z2R_mult. rewrite Ztrunc_Z2R. auto.
-  + unfold F2R; simpl. rewrite Z2R_cond_Zopp. rewrite <- cond_Ropp_mult_l.
-    assert (EQ: forall x, Ztrunc (cond_Ropp b x) = cond_Zopp b (Ztrunc x)).
+  + unfold F2R; simpl. rewrite Rmult_1_r. rewrite Ztrunc_IZR. auto.
+  + unfold F2R; simpl. rewrite <- mult_IZR. rewrite Ztrunc_IZR. auto.
+  + unfold F2R; simpl. rewrite IZR_cond_Zopp. rewrite <- cond_Ropp_mult_l.
+    assert (EQ: forall x, Ztrunc (cond_Ropp s x) = cond_Zopp s (Ztrunc x)).
     {
-      intros. destruct b; simpl; auto. apply Ztrunc_opp.
+      intros. destruct s; simpl; auto. apply Ztrunc_opp.
     }
     rewrite EQ. f_equal.
     generalize (Zpower_pos_gt_0 2 p (eq_refl _)); intros.
     rewrite Ztrunc_floor. symmetry. apply Zfloor_div. omega.
-    apply Rmult_le_pos. apply (Z2R_le 0). compute; congruence.
-    apply Rlt_le. apply Rinv_0_lt_compat. apply (Z2R_lt 0). auto.
+    apply Rmult_le_pos. apply IZR_le. compute; congruence.
+    apply Rlt_le. apply Rinv_0_lt_compat. apply IZR_lt. auto.
 Qed.
 
 (** Interval properties. *)
 
 Remark Ztrunc_range_pos:
-  forall x, 0 < Ztrunc x -> (Z2R (Ztrunc x) <= x < Z2R (Ztrunc x + 1)%Z)%R.
+  forall x, 0 < Ztrunc x -> (IZR (Ztrunc x) <= x < IZR (Ztrunc x + 1)%Z)%R.
 Proof.
   intros.
-  rewrite Ztrunc_floor. split. apply Zfloor_lb. rewrite Z2R_plus. apply Zfloor_ub.
+  rewrite Ztrunc_floor. split. apply Zfloor_lb. rewrite plus_IZR. apply Zfloor_ub.
   generalize (Rle_bool_spec 0%R x). intros RLE; inversion RLE; subst; clear RLE.
   auto.
   rewrite Ztrunc_ceil in H by lra. unfold Zceil in H.
   assert (-x < 0)%R.
-  { apply Rlt_le_trans with (Z2R (Zfloor (-x)) + 1)%R. apply Zfloor_ub.
-    change 0%R with (Z2R 0). change 1%R with (Z2R 1). rewrite <- Z2R_plus.
-    apply Z2R_le. omega. }
+  { apply Rlt_le_trans with (IZR (Zfloor (-x)) + 1)%R. apply Zfloor_ub.
+    rewrite <- plus_IZR.
+    apply IZR_le. omega. }
   lra.
 Qed.
 
@@ -744,32 +737,32 @@ Proof.
   intros; generalize (Rle_bool_spec 0%R x). intros RLE; inversion RLE; subst; clear RLE.
 - rewrite Ztrunc_floor in H by auto. split.
   + apply Rlt_le_trans with 0%R; auto. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply Rlt_0_1.
-  + replace 1%R with (Z2R (Zfloor x) + 1)%R. apply Zfloor_ub. rewrite H. simpl. apply Rplus_0_l.
+  + replace 1%R with (IZR (Zfloor x) + 1)%R. apply Zfloor_ub. rewrite H. simpl. apply Rplus_0_l.
 - rewrite Ztrunc_ceil in H by (apply Rlt_le; auto). split.
   + apply (Ropp_lt_cancel (-(1))). rewrite Ropp_involutive.
-    replace 1%R with (Z2R (Zfloor (-x)) + 1)%R. apply Zfloor_ub.
+    replace 1%R with (IZR (Zfloor (-x)) + 1)%R. apply Zfloor_ub.
     unfold Zceil in H. replace (Zfloor (-x)) with 0 by omega. simpl. apply Rplus_0_l.
   + apply Rlt_le_trans with 0%R; auto. apply Rle_0_1.
 Qed.
 
 Theorem ZofB_range_pos:
-  forall f n, ZofB f = Some n -> 0 < n -> (Z2R n <= B2R _ _ f < Z2R (n + 1)%Z)%R.
+  forall f n, ZofB f = Some n -> 0 < n -> (IZR n <= B2R _ _ f < IZR (n + 1)%Z)%R.
 Proof.
   intros. rewrite ZofB_correct in H. destruct (is_finite prec emax f) eqn:FIN; inversion H.
   apply Ztrunc_range_pos. congruence.
 Qed.
 
 Theorem ZofB_range_neg:
-  forall f n, ZofB f = Some n -> n < 0 -> (Z2R (n - 1)%Z < B2R _ _ f <= Z2R n)%R.
+  forall f n, ZofB f = Some n -> n < 0 -> (IZR (n - 1)%Z < B2R _ _ f <= IZR n)%R.
 Proof.
   intros. rewrite ZofB_correct in H. destruct (is_finite prec emax f) eqn:FIN; inversion H.
   set (x := B2R prec emax f) in *. set (y := (-x)%R).
-  assert (A: (Z2R (Ztrunc y) <= y < Z2R (Ztrunc y + 1)%Z)%R).
+  assert (A: (IZR (Ztrunc y) <= y < IZR (Ztrunc y + 1)%Z)%R).
   { apply Ztrunc_range_pos. unfold y. rewrite Ztrunc_opp. omega. }
   destruct A as [B C].
   unfold y in B, C. rewrite Ztrunc_opp in B, C.
   replace (- Ztrunc x + 1) with (- (Ztrunc x - 1)) in C by omega.
-  rewrite Z2R_opp in B, C. lra.
+  rewrite opp_IZR in B, C. lra.
 Qed.
 
 Theorem ZofB_range_zero:
@@ -780,13 +773,13 @@ Proof.
 Qed.
 
 Theorem ZofB_range_nonneg:
-  forall f n, ZofB f = Some n -> 0 <= n -> (-1 < B2R _ _ f < Z2R (n + 1)%Z)%R.
+  forall f n, ZofB f = Some n -> 0 <= n -> (-1 < B2R _ _ f < IZR (n + 1)%Z)%R.
 Proof.
   intros. destruct (Z.eq_dec n 0).
 - subst n. apply ZofB_range_zero. auto.
 - destruct (ZofB_range_pos f n) as (A & B). auto. omega.
-  split; auto. apply Rlt_le_trans with (Z2R 0). simpl; lra.
-  apply Rle_trans with (Z2R n); auto. apply Z2R_le; auto.
+  split; auto. apply Rlt_le_trans with 0%R. simpl; lra.
+  apply Rle_trans with (IZR n); auto. apply IZR_le; auto.
 Qed.
 
 (** For representable integers, [ZofB] is left inverse of [BofZ]. *)
@@ -795,35 +788,35 @@ Theorem ZofBofZ_exact:
   forall n, integer_representable n -> ZofB (BofZ n) = Some n.
 Proof.
   intros. destruct (BofZ_representable n H) as (A & B & C).
-  rewrite ZofB_correct. rewrite A, B. f_equal. apply Ztrunc_Z2R.
+  rewrite ZofB_correct. rewrite A, B. f_equal. apply Ztrunc_IZR.
 Qed.
 
 (** Compatibility with subtraction *)
 
 Remark Zfloor_minus:
-  forall x n, Zfloor (x - Z2R n) = Zfloor x - n.
+  forall x n, Zfloor (x - IZR n) = Zfloor x - n.
 Proof.
   intros. apply Zfloor_imp. replace (Zfloor x - n + 1) with ((Zfloor x + 1) - n) by omega.
-  rewrite ! Z2R_minus. unfold Rminus. split.
+  rewrite ! minus_IZR. unfold Rminus. split.
   apply Rplus_le_compat_r. apply Zfloor_lb.
-  apply Rplus_lt_compat_r. rewrite Z2R_plus. apply Zfloor_ub.
+  apply Rplus_lt_compat_r. rewrite plus_IZR. apply Zfloor_ub.
 Qed.
 
 Theorem ZofB_minus:
   forall minus_nan m f p q,
-  ZofB f = Some p -> 0 <= p < 2*q -> q <= 2^prec -> (Z2R q <= B2R _ _ f)%R ->
+  ZofB f = Some p -> 0 <= p < 2*q -> q <= 2^prec -> (IZR q <= B2R _ _ f)%R ->
   ZofB (Bminus _ _ _ Hmax minus_nan m f (BofZ q)) = Some (p - q).
 Proof.
   intros.
   assert (Q: -2^prec <= q <= 2^prec).
   { split; auto.  generalize (Zpower_ge_0 radix2 prec); simpl; omega. }
-  assert (RANGE: (-1 < B2R _ _ f < Z2R (p + 1)%Z)%R) by (apply ZofB_range_nonneg; auto; omega).
+  assert (RANGE: (-1 < B2R _ _ f < IZR (p + 1)%Z)%R) by (apply ZofB_range_nonneg; auto; omega).
   rewrite ZofB_correct in H. destruct (is_finite prec emax f) eqn:FIN; try discriminate.
-  assert (PQ2: (Z2R (p + 1) <= Z2R q * 2)%R).
-  { change 2%R with (Z2R 2). rewrite <- Z2R_mult. apply Z2R_le. omega. }
-  assert (EXACT: round radix2 fexp (round_mode m) (B2R _ _ f - Z2R q)%R = (B2R _ _ f - Z2R q)%R).
+  assert (PQ2: (IZR (p + 1) <= IZR q * 2)%R).
+  { rewrite <- mult_IZR. apply IZR_le. omega. }
+  assert (EXACT: round radix2 fexp (round_mode m) (B2R _ _ f - IZR q)%R = (B2R _ _ f - IZR q)%R).
   { apply round_generic. apply valid_rnd_round_mode.
-    apply sterbenz_aux. apply FLT_exp_monotone. apply generic_format_B2R.
+    apply sterbenz_aux. now apply FLT_exp_valid. apply FLT_exp_monotone. apply generic_format_B2R.
     apply integer_representable_n. auto. lra. }
   destruct (BofZ_exact q Q) as (A & B & C).
   generalize (Bminus_correct _ _ _ Hmax minus_nan m f (BofZ q) FIN B).
@@ -834,8 +827,8 @@ Proof.
   lra. lra.
 - rewrite A. fold emin; fold fexp. rewrite EXACT.
   apply Rle_lt_trans with (bpow radix2 prec).
-  apply Rle_trans with (Z2R q). apply Rabs_le. lra.
-  rewrite <- Z2R_Zpower. apply Z2R_le; auto. red in prec_gt_0_; omega.
+  apply Rle_trans with (IZR q). apply Rabs_le. lra.
+  rewrite <- IZR_Zpower. apply IZR_le; auto. red in prec_gt_0_; omega.
   apply bpow_lt. auto.
 Qed.
 
@@ -875,7 +868,7 @@ Qed.
 
 Theorem ZofB_range_minus:
   forall minus_nan m f p q,
-  ZofB_range f 0 (2 * q - 1) = Some p -> q <= 2^prec -> (Z2R q <= B2R _ _ f)%R ->
+  ZofB_range f 0 (2 * q - 1) = Some p -> q <= 2^prec -> (IZR q <= B2R _ _ f)%R ->
   ZofB_range (Bminus _ _ _ Hmax minus_nan m f (BofZ q)) (-q) (q - 1) = Some (p - q).
 Proof.
   intros. destruct (ZofB_range_inversion _ _ _ _ H) as (A & B & C).
@@ -897,11 +890,11 @@ Proof.
   intros until y; intros NAN.
   pose proof (Bplus_correct _ _ _ Hmax plus_nan mode x y).
   pose proof (Bplus_correct _ _ _ Hmax plus_nan mode y x).
-  unfold Bplus in *; destruct x; destruct y; auto.
-- rewrite (eqb_sym b0 b). destruct (eqb b b0) eqn:EQB; auto.
+  unfold Bplus in *; destruct x as [sx|sx|sx px Hx|sx mx ex Hx]; destruct y as [sy|sy|sy py Hy|sy my ey Hy]; auto.
+- rewrite (eqb_sym sy sx). destruct (eqb sx sy) eqn:EQB; auto.
   f_equal; apply eqb_prop; auto.
 - rewrite NAN; auto.
-- rewrite (eqb_sym b0 b). destruct (eqb b b0) eqn:EQB.
+- rewrite (eqb_sym sy sx). destruct (eqb sx sy) eqn:EQB.
   f_equal; apply eqb_prop; auto.
   rewrite NAN; auto.
 - rewrite NAN; auto.
@@ -913,8 +906,8 @@ Proof.
 - generalize (H (eq_refl _) (eq_refl _)); clear H.
   generalize (H0 (eq_refl _) (eq_refl _)); clear H0.
   fold emin. fold fexp.
-  set (x := B754_finite prec emax b0 m0 e1 e2). set (rx := B2R _ _ x).
-  set (y := B754_finite prec emax b m e e0). set (ry := B2R _ _ y).
+  set (x := B754_finite prec emax sx mx ex Hx). set (rx := B2R _ _ x).
+  set (y := B754_finite prec emax sy my ey Hy). set (ry := B2R _ _ y).
   rewrite (Rplus_comm ry rx). destruct Rlt_bool.
   + intros (A1 & A2 & A3) (B1 & B2 & B3).
     apply B2R_Bsign_inj; auto. rewrite <- B1 in A1. auto.
@@ -930,31 +923,31 @@ Proof.
   intros until y; intros NAN.
   pose proof (Bmult_correct _ _ _ Hmax mult_nan mode x y).
   pose proof (Bmult_correct _ _ _ Hmax mult_nan mode y x).
-  unfold Bmult in *; destruct x; destruct y; auto.
-- rewrite (xorb_comm b0 b); auto.
+  unfold Bmult in *; destruct x as [sx|sx|sx px Hx|sx mx ex Hx]; destruct y as [sy|sy|sy py Hy|sy my ey Hy]; auto.
+- rewrite (xorb_comm sx sy); auto.
 - rewrite NAN; auto.
 - rewrite NAN; auto.
-- rewrite (xorb_comm b0 b); auto.
+- rewrite (xorb_comm sx sy); auto.
 - rewrite NAN; auto.
-- rewrite (xorb_comm b0 b); auto.
+- rewrite (xorb_comm sx sy); auto.
 - rewrite NAN; auto.
-- rewrite (xorb_comm b0 b); auto.
+- rewrite (xorb_comm sx sy); auto.
 - rewrite NAN; auto.
 - rewrite NAN; auto.
 - rewrite NAN; auto.
 - rewrite NAN; auto.
-- rewrite (xorb_comm b0 b); auto.
-- rewrite (xorb_comm b0 b); auto.
+- rewrite (xorb_comm sx sy); auto.
+- rewrite (xorb_comm sx sy); auto.
 - rewrite NAN; auto.
 - revert H H0. fold emin. fold fexp.
-  set (x := B754_finite prec emax b0 m0 e1 e2). set (rx := B2R _ _ x).
-  set (y := B754_finite prec emax b m e e0). set (ry := B2R _ _ y).
+  set (x := B754_finite prec emax sx mx ex Hx). set (rx := B2R _ _ x).
+  set (y := B754_finite prec emax sy my ey Hy). set (ry := B2R _ _ y).
   rewrite (Rmult_comm ry rx).
   destruct (Rlt_bool (Rabs (round radix2 fexp (round_mode mode) (rx * ry)))
                      (bpow radix2 emax)).
   + intros (A1 & A2 & A3) (B1 & B2 & B3).
     apply B2R_Bsign_inj; auto. rewrite <- B1 in A1. auto.
-    rewrite ! Bsign_FF2B. f_equal. f_equal. apply xorb_comm. apply Pos.mul_comm. apply Z.add_comm.
+    rewrite ! Bsign_FF2B. f_equal. f_equal. apply xorb_comm. now rewrite Pos.mul_comm. apply Z.add_comm.
   + intros A B. apply B2FF_inj. etransitivity. eapply A. rewrite xorb_comm. auto.
 Qed.
 
@@ -973,26 +966,26 @@ Proof.
   rewrite A, B, C in H. rewrite xorb_false_r in H.
   destruct (is_finite _ _ f) eqn:FIN.
 - pose proof (Bplus_correct _ _ _ Hmax plus_nan mode f f FIN FIN). fold emin in H0.
-  assert (EQ: (B2R prec emax f * Z2R 2%Z = B2R prec emax f + B2R prec emax f)%R).
-  { change (Z2R 2%Z) with 2%R. ring. }
+  assert (EQ: (B2R prec emax f * IZR 2%Z = B2R prec emax f + B2R prec emax f)%R).
+  { ring. }
   rewrite <- EQ in H0. destruct Rlt_bool.
   + destruct H0 as (P & Q & R). destruct H as (S & T & U).
     apply B2R_Bsign_inj; auto.
     rewrite P, S. auto.
     rewrite R, U.
-    replace 0%R with (0 * Z2R 2%Z)%R by ring. rewrite Rcompare_mult_r.
-    rewrite andb_diag, orb_diag. destruct f; try discriminate; simpl.
+    replace 0%R with (0 * 2)%R by ring. rewrite Rcompare_mult_r.
+    rewrite andb_diag, orb_diag. destruct f as [s|s|s p H|s m e H]; try discriminate; simpl.
     rewrite Rcompare_Eq by auto. destruct mode; auto.
     replace 0%R with (@F2R radix2 {| Fnum := 0%Z; Fexp := e |}).
-    rewrite Rcompare_F2R. destruct b; auto.
+    rewrite Rcompare_F2R. destruct s; auto.
     unfold F2R. simpl. ring.
-    change 0%R with (Z2R 0%Z). apply Z2R_lt. omega.
+    apply IZR_lt. omega.
     destruct (Bmult prec emax prec_gt_0_ Hmax mult_nan mode f (BofZ 2)); reflexivity || discriminate.
   + destruct H0 as (P & Q). apply B2FF_inj. rewrite P, H. auto.
-- destruct f; try discriminate.
-  + simpl Bplus. rewrite eqb_true. destruct (BofZ 2) eqn:B2; try discriminate; simpl in *.
-    assert ((0 = 2)%Z) by (apply eq_Z2R; auto). discriminate.
-    subst b0. rewrite xorb_false_r. auto.
+- destruct f as [sf|sf|sf pf Hf|sf mf ef Hf]; try discriminate.
+  + simpl Bplus. rewrite eqb_true. destruct (BofZ 2) as [| | |s2 m2 e2 H2] eqn:B2; try discriminate; simpl in *.
+    assert ((0 = 2)%Z) by (apply eq_IZR; auto). discriminate.
+    subst s2. rewrite xorb_false_r. auto.
     auto.
   + unfold Bplus, Bmult. rewrite <- NAN by auto. auto.
 Qed.
@@ -1031,7 +1024,7 @@ Remark bounded_Bexact_inverse:
   forall e,
   emin <= e <= emax - prec <-> bounded prec emax Bexact_inverse_mantissa e = true.
 Proof.
-  intros. unfold bounded, canonic_mantissa. rewrite andb_true_iff.
+  intros. unfold bounded, canonical_mantissa. rewrite andb_true_iff.
   rewrite <- Zeq_is_eq_bool. rewrite <- Zle_is_le_bool.
   rewrite Bexact_inverse_mantissa_digits2_pos.
   split.
@@ -1063,23 +1056,23 @@ Lemma Bexact_inverse_correct:
   /\ B2R _ _ f <> 0%R
   /\ Bsign _ _ f' = Bsign _ _ f.
 Proof with (try discriminate).
-  intros f f' EI. unfold Bexact_inverse in EI. destruct f...
+  intros f f' EI. unfold Bexact_inverse in EI. destruct f as [s|s|s p H|s m e H]...
   destruct (Pos.eq_dec m Bexact_inverse_mantissa)...
   set (e' := -e - (prec - 1) * 2) in *.
   destruct (Z_le_dec emin e')...
   destruct (Z_le_dec e' emax)...
   inversion EI; clear EI; subst f' m.
   split. auto. split. auto. split. unfold B2R. rewrite Bexact_inverse_mantissa_value.
-  unfold F2R; simpl. rewrite Z2R_cond_Zopp.
+  unfold F2R; simpl. rewrite IZR_cond_Zopp.
   rewrite <- ! cond_Ropp_mult_l.
   red in prec_gt_0_.
-  replace (Z2R (2 ^ (prec - 1))) with (bpow radix2 (prec - 1))
-  by (symmetry; apply (Z2R_Zpower radix2); omega).
+  replace (IZR (2 ^ (prec - 1))) with (bpow radix2 (prec - 1))
+  by (symmetry; apply (IZR_Zpower radix2); omega).
   rewrite <- ! bpow_plus.
   replace (prec - 1 + e') with (- (prec - 1 + e)) by (unfold e'; omega).
-  rewrite bpow_opp. unfold cond_Ropp; destruct b; auto.
+  rewrite bpow_opp. unfold cond_Ropp; destruct s; auto.
   rewrite Ropp_inv_permute. auto. apply Rgt_not_eq. apply bpow_gt_0.
-  split. simpl. red; intros. apply F2R_eq_0_reg in H. destruct b; simpl in H; discriminate.
+  split. simpl. apply F2R_neq_0. destruct s; simpl in H; discriminate.
   auto.
 Qed.
 
@@ -1180,7 +1173,7 @@ Lemma bpow_log_pos:
   0 < n ->
   (bpow radix2 (n * Z.log2 base)%Z <= bpow base n)%R.
 Proof.
-  intros. rewrite <- ! Z2R_Zpower. apply Z2R_le; apply Zpower_log; auto.
+  intros. rewrite <- ! IZR_Zpower. apply IZR_le; apply Zpower_log; auto.
   omega.
   rewrite Z.mul_comm; apply Zmult_gt_0_le_0_compat. omega. apply Z.log2_nonneg.
 Qed.
@@ -1202,7 +1195,7 @@ Lemma round_integer_overflow:
   forall (base: radix) e m,
   0 < e ->
   emax <= e * Z.log2 base ->
-  (bpow radix2 emax <= round radix2 fexp (round_mode mode_NE) (Z2R (Zpos m) * bpow base e))%R.
+  (bpow radix2 emax <= round radix2 fexp (round_mode mode_NE) (IZR (Zpos m) * bpow base e))%R.
 Proof.
   intros.
   rewrite <- (round_generic radix2 fexp (round_mode mode_NE) (bpow radix2 emax)); auto.
@@ -1210,11 +1203,11 @@ Proof.
   rewrite <- (Rmult_1_l (bpow radix2 emax)). apply Rmult_le_compat.
   apply Rle_0_1.
   apply bpow_ge_0.
-  apply (Z2R_le 1). zify; omega.
+  apply IZR_le. zify; omega.
   eapply Rle_trans. eapply bpow_le. eassumption. apply bpow_log_pos; auto.
   apply generic_format_FLT. exists (Float radix2 1 emax).
-  split. unfold F2R; simpl. ring.
-  split. simpl. apply (Zpower_gt_1 radix2); auto.
+  unfold F2R; simpl. ring.
+  simpl. apply (Zpower_gt_1 radix2); auto.
   simpl. unfold emin; red in prec_gt_0_; omega.
 Qed.
 
@@ -1227,15 +1220,15 @@ Proof.
   set (eps := bpow radix2 (emin - 1)) in *.
   assert (A: round radix2 fexp (round_mode mode_NE) eps = 0%R).
   { unfold round. simpl.
-    assert (E: canonic_exp radix2 fexp eps = emin).
-    { unfold canonic_exp, eps. rewrite ln_beta_bpow. unfold fexp, FLT_exp. zify; red in prec_gt_0_; omega. }
+    assert (E: cexp radix2 fexp eps = emin).
+    { unfold cexp, eps. rewrite mag_bpow. unfold fexp, FLT_exp. zify; red in prec_gt_0_; omega. }
     unfold scaled_mantissa; rewrite E.
     assert (P: (eps * bpow radix2 (-emin) = / 2)%R).
     { unfold eps. rewrite <- bpow_plus. replace (emin - 1 + -emin) with (-1) by omega. auto. }
     rewrite P. unfold Znearest.
     assert (F: Zfloor (/ 2)%R = 0).
     { apply Zfloor_imp. simpl. lra. }
-    rewrite F. change (Z2R 0) with 0%R. rewrite Rminus_0_r. rewrite Rcompare_Eq by auto.
+    rewrite F. rewrite Rminus_0_r. rewrite Rcompare_Eq by auto.
     simpl. unfold F2R; simpl. apply Rmult_0_l.
   }
   apply Rle_antisym.
@@ -1248,15 +1241,15 @@ Lemma round_integer_underflow:
   forall (base: radix) e m,
   e < 0 ->
   e * Z.log2 base + Z.log2_up (Zpos m) < emin ->
-  round radix2 fexp (round_mode mode_NE) (Z2R (Zpos m) * bpow base e) = 0%R.
+  round radix2 fexp (round_mode mode_NE) (IZR (Zpos m) * bpow base e) = 0%R.
 Proof.
   intros. apply round_NE_underflows. split.
-- apply Rmult_le_pos. apply (Z2R_le 0). zify; omega. apply bpow_ge_0.
+- apply Rmult_le_pos. apply IZR_le. zify; omega. apply bpow_ge_0.
 - apply Rle_trans with (bpow radix2 (Z.log2_up (Z.pos m) + e * Z.log2 base)).
 + rewrite bpow_plus. apply Rmult_le_compat.
-  apply (Z2R_le 0); zify; omega.
+  apply IZR_le; zify; omega.
   apply bpow_ge_0.
-  rewrite <- Z2R_Zpower. apply Z2R_le.
+  rewrite <- IZR_Zpower. apply IZR_le.
   destruct (Z.eq_dec (Z.pos m) 1).
   rewrite e0. simpl. omega.
   apply Z.log2_up_spec. zify; omega.
@@ -1270,7 +1263,7 @@ Qed.
 Theorem Bparse_correct:
   forall b m e (BASE: 2 <= Zpos b),
   let base := {| radix_val := Zpos b; radix_prop := Zle_imp_le_bool _ _ BASE |} in
-  let r := round radix2 fexp (round_mode mode_NE) (Z2R (Zpos m) * bpow base e) in
+  let r := round radix2 fexp (round_mode mode_NE) (IZR (Zpos m) * bpow base e) in
   if Rlt_bool (Rabs r) (bpow radix2 emax) then
      B2R _ _ (Bparse b m e) = r
   /\ is_finite _ _ (Bparse b m e) = true
@@ -1279,7 +1272,7 @@ Theorem Bparse_correct:
     B2FF _ _ (Bparse b m e) = F754_infinity false.
 Proof.
   intros.
-  assert (A: forall x, @F2R radix2 {| Fnum := x; Fexp := 0 |} = Z2R x).
+  assert (A: forall x, @F2R radix2 {| Fnum := x; Fexp := 0 |} = IZR x).
   { intros. unfold F2R, Fnum; simpl. ring. }
   unfold Bparse, r. destruct e as [ | e | e].
 - (* e = Z0 *)
@@ -1288,7 +1281,7 @@ Proof.
 - (* e = Zpos e *)
   destruct (Z.ltb_spec (Z.pos e * Z.log2 (Z.pos b)) emax).
 + (* no overflow *)
-  rewrite pos_pow_spec. rewrite <- Z2R_Zpower by (zify; omega). rewrite <- Z2R_mult.
+  rewrite pos_pow_spec. rewrite <- IZR_Zpower by (zify; omega). rewrite <- mult_IZR.
   replace false with (Z.pos m * Z.pos b ^ Z.pos e <? 0).
   exact (BofZ_correct (Z.pos m * Z.pos b ^ Z.pos e)).
   rewrite Z.ltb_ge. rewrite Z.mul_comm. apply Zmult_gt_0_le_0_compat. zify; omega.  apply (Zpower_ge_0 base).
@@ -1300,25 +1293,21 @@ Proof.
 + (* undeflow *)
   rewrite round_integer_underflow; auto.
   rewrite Rlt_bool_true. auto.
-  replace (Rabs 0)%R with 0%R. apply bpow_gt_0. apply (Z2R_abs 0).
+  replace (Rabs 0)%R with 0%R. apply bpow_gt_0. apply (abs_IZR 0).
   zify; omega.
 + (* no underflow *)
   generalize (Bdiv_correct_aux prec emax prec_gt_0_ Hmax mode_NE false m 0 false (pos_pow b e) 0).
-  set (f := match Fdiv_core_binary prec (Z.pos m) 0 (Z.pos (pos_pow b e)) 0 with
-      | (0, _, _) => F754_nan false 1
-      | (Z.pos mz0, ez, lz) =>
-          binary_round_aux prec emax mode_NE (xorb false false) mz0 ez lz
-      | (Z.neg _, _, _) => F754_nan false 1
-      end).
+  set (f := let '(mz, ez, lz) := Fdiv_core_binary prec emax (Z.pos m) 0 (Z.pos (pos_pow b e)) 0
+         in binary_round_aux prec emax mode_NE (xorb false false) mz ez lz).
   fold emin; fold fexp. rewrite ! A. unfold cond_Zopp. rewrite pos_pow_spec.
-  assert (B: (Z2R (Z.pos m) / Z2R (Z.pos b ^ Z.pos e) =
-              Z2R (Z.pos m) * bpow base (Z.neg e))%R).
+  assert (B: (IZR (Z.pos m) / IZR (Z.pos b ^ Z.pos e) =
+              IZR (Z.pos m) * bpow base (Z.neg e))%R).
   { change (Z.neg e) with (- (Z.pos e)). rewrite bpow_opp. auto. }
   rewrite B. intros [P Q].
   destruct (Rlt_bool
      (Rabs
         (round radix2 fexp (round_mode mode_NE)
-           (Z2R (Z.pos m) * bpow base (Z.neg e))))
+           (IZR (Z.pos m) * bpow base (Z.neg e))))
     (bpow radix2 emax)).
 * destruct Q as (Q1 & Q2 & Q3).
   split. rewrite B2R_FF2B, Q1. auto.
@@ -1344,9 +1333,9 @@ Hypothesis Hmax2 : (prec2 < emax2)%Z.
 Let binary_float1 := binary_float prec1 emax1.
 Let binary_float2 := binary_float prec2 emax2.
 
-Definition Bconv (conv_nan: bool -> nan_pl prec1 -> bool * nan_pl prec2) (md: mode) (f: binary_float1) : binary_float2 :=
+Definition Bconv (conv_nan: binary_float1 -> {x | is_nan prec2 emax2 x = true}) (md: mode) (f: binary_float1) : binary_float2 :=
   match f with
-    | B754_nan _ _ s pl => let '(s, pl) := conv_nan s pl in B754_nan _ _ s pl
+    | B754_nan _ _ _ _ _ => build_nan prec2 emax2 (conv_nan f)
     | B754_infinity _ _ s => B754_infinity _ _ s
     | B754_zero _ _ s => B754_zero _ _ s
     | B754_finite _ _ s m e _ => binary_normalize _ _ _ Hmax2 md (cond_Zopp s (Zpos m)) e s
@@ -1363,18 +1352,18 @@ Theorem Bconv_correct:
   else
      B2FF _ _ (Bconv conv_nan m f) = binary_overflow prec2 emax2 m (Bsign _ _ f).
 Proof.
-  intros. destruct f; try discriminate.
+  intros. destruct f as [sf|sf|sf pf Hf|sf mf ef Hf]; try discriminate.
 - simpl. rewrite round_0. rewrite Rabs_R0. rewrite Rlt_bool_true. auto.
   apply bpow_gt_0. apply valid_rnd_round_mode.
-- generalize (binary_normalize_correct _ _ _ Hmax2 m (cond_Zopp b (Zpos m0)) e b).
+- generalize (binary_normalize_correct _ _ _ Hmax2 m (cond_Zopp sf (Zpos mf)) ef sf).
   fold emin2; fold fexp2. simpl. destruct Rlt_bool.
   + intros (A & B & C). split. auto. split. auto. rewrite C.
-    destruct b; simpl.
-    rewrite Rcompare_Lt. auto. apply F2R_lt_0_compat. simpl. compute; auto.
-    rewrite Rcompare_Gt. auto. apply F2R_gt_0_compat. simpl. compute; auto.
-  + intros A. rewrite A. f_equal. destruct b.
-    apply Rlt_bool_true. apply F2R_lt_0_compat. simpl. compute; auto.
-    apply Rlt_bool_false. apply Rlt_le. apply Rgt_lt. apply F2R_gt_0_compat. simpl. compute; auto.
+    destruct sf; simpl.
+    rewrite Rcompare_Lt. auto. apply F2R_lt_0. simpl. compute; auto.
+    rewrite Rcompare_Gt. auto. apply F2R_gt_0. simpl. compute; auto.
+  + intros A. rewrite A. f_equal. destruct sf.
+    apply Rlt_bool_true. apply F2R_lt_0. simpl. compute; auto.
+    apply Rlt_bool_false. apply Rlt_le. apply Rgt_lt. apply F2R_gt_0. simpl. compute; auto.
 Qed.
 
 (** Converting a finite FP number to higher or equal precision preserves its value. *)
@@ -1421,15 +1410,15 @@ Proof.
   unfold BofZ.
   generalize (binary_normalize_correct _ _ _ Hmax2 mode_NE n 0 false).
   fold emin2; fold fexp2. rewrite A.
-  replace (F2R {| Fnum := n; Fexp := 0 |}) with (Z2R n).
+  replace (F2R {| Fnum := n; Fexp := 0 |}) with (IZR n).
   destruct Rlt_bool.
 - intros (P & Q & R) (D & E & F). apply B2R_Bsign_inj; auto.
-  congruence. rewrite F, C, R. change 0%R with (Z2R 0). rewrite Rcompare_Z2R.
+  congruence. rewrite F, C, R. rewrite Rcompare_IZR.
   unfold Z.ltb. auto.
-- intros P Q. apply B2FF_inj. rewrite P, Q. rewrite C. f_equal. change 0%R with (Z2R 0).
+- intros P Q. apply B2FF_inj. rewrite P, Q. rewrite C. f_equal.
   generalize (Zlt_bool_spec n 0); intros LT; inversion LT.
-  rewrite Rlt_bool_true; auto. apply Z2R_lt; auto.
-  rewrite Rlt_bool_false; auto. apply Z2R_le; auto.
+  rewrite Rlt_bool_true; auto. apply IZR_lt; auto.
+  rewrite Rlt_bool_false; auto. apply IZR_le; auto.
 - unfold F2R; simpl. rewrite Rmult_1_r. auto.
 Qed.
 
@@ -1472,19 +1461,15 @@ Proof.
   rewrite ! Bcompare_correct by auto. rewrite A, D. auto.
 - generalize (Bconv_widen_exact H H0 conv_nan m x)
              (Bconv_widen_exact H H0 conv_nan m y); intros P Q.
-  destruct x, y; try discriminate; simpl in P, Q; simpl;
+  destruct x as [sx|sx|sx px Hx|sx mx ex Hx], y as [sy|sy|sy py Hy|sy my ey Hy]; try discriminate; simpl in P, Q; simpl;
   repeat (match goal with |- context [conv_nan ?b ?pl] => destruct (conv_nan b pl) end);
   auto.
   destruct Q as (D & E & F); auto.
-  destruct (binary_normalize prec2 emax2 prec2_gt_0_ Hmax2 m (cond_Zopp b0 (Z.pos m0)) e b0);
-  discriminate || reflexivity.
+  now destruct binary_normalize.
   destruct P as (A & B & C); auto.
-  destruct (binary_normalize prec2 emax2 prec2_gt_0_ Hmax2 m (cond_Zopp b (Z.pos m0)) e b);
-  try discriminate; simpl. destruct b; auto. destruct b, b1; auto.
+  now destruct binary_normalize.
   destruct P as (A & B & C); auto.
-  destruct (binary_normalize prec2 emax2 prec2_gt_0_ Hmax2 m (cond_Zopp b (Z.pos m0)) e b);
-  try discriminate; simpl. destruct b; auto.
-  destruct b, b2; auto.
+  now destruct binary_normalize.
 Qed.
 
 End Conversions.
diff --git a/lib/Floats.v b/lib/Floats.v
index ba225be1..0247528c 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -18,10 +18,9 @@
 
 Require Import Coqlib.
 Require Import Integers.
-Require Import Fappli_IEEE.
-Require Import Fappli_IEEE_bits.
+(*From Flocq*)
+Require Import Binary Bits Core.
 Require Import Fappli_IEEE_extra.
-Require Import Fcore.
 Require Import Program.
 Require Archi.
 
@@ -111,77 +110,84 @@ Module Float.
 
 (** Transform a Nan payload to a quiet Nan payload. *)
 
-Program Definition transform_quiet_pl (pl:nan_pl 53) : nan_pl 53 :=
-  Pos.lor pl (iter_nat xO 51 xH).
-Next Obligation.
-  destruct pl.
+Lemma transform_quiet_nan_proof (p : positive) :
+  nan_pl 53 p = true ->
+  nan_pl 53 (Pos.lor p (iter_nat xO 51 1%positive)) = true.
+Proof.
+  unfold nan_pl. intros K.
   simpl. rewrite Z.ltb_lt in *.
-  assert (forall x, Fcore_digits.digits2_pos x = Pos.size x).
-  { induction x0; simpl; auto; rewrite IHx0; zify; omega. }
+  assert (H : forall x, Digits.digits2_pos x = Pos.size x).
+  { induction x; simpl; auto; rewrite IHx; zify; omega. }
   rewrite H, Psize_log_inf, <- Zlog2_log_inf in *. clear H.
-  change (Z.pos (Pos.lor x 2251799813685248)) with (Z.lor (Z.pos x) 2251799813685248%Z).
+  change (Z.pos (Pos.lor p 2251799813685248)) with (Z.lor (Z.pos p) 2251799813685248%Z).
   rewrite Z.log2_lor by (zify; omega).
-  apply Z.max_case. auto. simpl. omega.
+  now apply Z.max_case.
 Qed.
 
-Lemma nan_payload_fequal:
-  forall prec (p1 p2: nan_pl prec),
-  proj1_sig p1 = proj1_sig p2 -> p1 = p2.
-Proof.
-  intros. destruct p1, p2; simpl in H; subst. f_equal. apply Fcore_Zaux.eqbool_irrelevance.
-Qed.
+Definition transform_quiet_nan s p H : {x :float | is_nan _ _ x = true} :=
+  exist _ (B754_nan 53 1024 s _ (transform_quiet_nan_proof p H)) (eq_refl true).
+
+(** Nan payload operations for single <-> double conversions. *)
 
-Lemma lor_idempotent:
-  forall x y, Pos.lor (Pos.lor x y) y = Pos.lor x y.
+Lemma expand_nan_proof (p : positive) :
+  nan_pl 24 p = true ->
+  nan_pl 53 (Pos.shiftl_nat p 29) = true.
 Proof.
-  induction x; destruct y; simpl; f_equal; auto;
-  induction y; simpl; f_equal; auto.
+  unfold nan_pl. intros K.
+  rewrite Z.ltb_lt in *.
+  unfold Pos.shiftl_nat, nat_rect, Digits.digits2_pos.
+  fold (Digits.digits2_pos p).
+  zify; omega.
 Qed.
 
-Lemma transform_quiet_pl_idempotent:
-  forall pl, transform_quiet_pl (transform_quiet_pl pl) = transform_quiet_pl pl.
+Definition expand_nan s p H : {x | is_nan 53 1024 x = true} :=
+  exist _ (B754_nan 53 1024 s _ (expand_nan_proof p H)) (eq_refl true).
+
+Definition of_single_nan (f : float32) : { x : float | is_nan _ _ x = true } :=
+  match f with
+  | B754_nan s p H =>
+    if Archi.float_of_single_preserves_sNaN
+    then expand_nan s p H
+    else transform_quiet_nan s _ (expand_nan_proof p H)
+  | _ => Archi.default_nan_64
+  end.
+
+Lemma reduce_nan_proof (p : positive) :
+  nan_pl 53 p = true ->
+  nan_pl 24 (Pos.shiftr_nat p 29) = true.
 Proof.
-  intros. apply nan_payload_fequal; simpl. apply lor_idempotent.
+  unfold nan_pl. intros K.
+  rewrite Z.ltb_lt in *.
+  unfold Pos.shiftr_nat, nat_rect.
+  assert (H : forall x, Digits.digits2_pos (Pos.div2 x) = (Digits.digits2_pos x - 1)%positive)
+    by (destruct x; simpl; auto; rewrite Pplus_one_succ_r, Pos.add_sub; auto).
+  rewrite !H, !Pos2Z.inj_sub_max.
+  repeat (apply Z.max_lub_lt; [reflexivity |apply Z.lt_sub_lt_add_l]).
+  exact K.
 Qed.
 
-(** Nan payload operations for single <-> double conversions. *)
+Definition reduce_nan s p H : {x : float32 | is_nan _ _ x = true} :=
+  exist _ (B754_nan 24 128 s _ (reduce_nan_proof p H)) (eq_refl true).
 
-Definition expand_pl (pl: nan_pl 24) : nan_pl 53.
-Proof.
-  refine (exist _ (Pos.shiftl_nat (proj1_sig pl) 29) _).
-  abstract (
-    destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_rect, Fcore_digits.digits2_pos;
-    fold (Fcore_digits.digits2_pos x);
-    rewrite Z.ltb_lt in *;
-    zify; omega).
-Defined.
-
-Definition of_single_pl (s:bool) (pl:nan_pl 24) : (bool * nan_pl 53) :=
-  (s,
-   if Archi.float_of_single_preserves_sNaN
-   then expand_pl pl
-   else transform_quiet_pl (expand_pl pl)).
-
-Definition reduce_pl (pl: nan_pl 53) : nan_pl 24.
-Proof.
-  refine (exist _ (Pos.shiftr_nat (proj1_sig pl) 29) _).
-  abstract (
-    destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_rect;
-    rewrite Z.ltb_lt in *;
-    assert (forall x, Fcore_digits.digits2_pos (Pos.div2 x) =
-                      (Fcore_digits.digits2_pos x - 1)%positive)
-      by (destruct x0; simpl; auto; rewrite Pplus_one_succ_r, Pos.add_sub; auto);
-    rewrite !H, !Pos2Z.inj_sub_max;
-    repeat (apply Z.max_lub_lt; [reflexivity |apply Z.lt_sub_lt_add_l]); auto).
-Defined.
-
-Definition to_single_pl (s:bool) (pl:nan_pl 53) : (bool * nan_pl 24) :=
-  (s, reduce_pl (transform_quiet_pl pl)).
+Definition to_single_nan (f : float) : { x : float32 | is_nan _ _ x = true } :=
+  match f with
+  | B754_nan s p H => reduce_nan s _ (transform_quiet_nan_proof p H)
+  | _ => Archi.default_nan_32
+  end.
 
 (** NaN payload operations for opposite and absolute value. *)
 
-Definition neg_pl (s:bool) (pl:nan_pl 53) := (negb s, pl).
-Definition abs_pl (s:bool) (pl:nan_pl 53) := (false, pl).
+Definition neg_nan (f : float) : { x : float | is_nan _ _ x = true } :=
+  match f with
+  | B754_nan s p H => exist _ (B754_nan 53 1024 (negb s) p H) (eq_refl true)
+  | _ => Archi.default_nan_64
+  end.
+
+Definition abs_nan (f : float) : { x : float | is_nan _ _ x = true } :=
+  match f with
+  | B754_nan s p H => exist _ (B754_nan 53 1024 false p H) (eq_refl true)
+  | _ => Archi.default_nan_64
+  end.
 
 (** The NaN payload operations for two-argument arithmetic operations
    are not part of the IEEE754 standard, but all architectures of
@@ -191,15 +197,16 @@ Definition abs_pl (s:bool) (pl:nan_pl 53) := (false, pl).
 - a choice function determining which of the payload arguments to choose,
   when an operation is given two NaN arguments. *)
 
-Definition binop_pl (x y: binary64) : bool*nan_pl 53 :=
+Definition binop_nan (x y : float) : {x : float | is_nan 53 1024 x = true} :=
+  if Archi.fpu_returns_default_qNaN then Archi.default_nan_64 else
   match x, y with
-  | B754_nan s1 pl1, B754_nan s2 pl2 =>
-      if Archi.choose_binop_pl_64 s1 pl1 s2 pl2
-      then (s2, transform_quiet_pl pl2)
-      else (s1, transform_quiet_pl pl1)
-  | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1)
-  | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2)
-  | _, _ => Archi.default_pl_64
+  | B754_nan s1 pl1 H1, B754_nan s2 pl2 H2 =>
+      if Archi.choose_binop_pl_64 pl1 pl2
+      then transform_quiet_nan s2 pl2 H2
+      else transform_quiet_nan s1 pl1 H1
+  | B754_nan s1 pl1 H1, _ => transform_quiet_nan s1 pl1 H1
+  | _, B754_nan s2 pl2 H2 => transform_quiet_nan s2 pl2 H2
+  | _, _ => Archi.default_nan_64
   end.
 
 (** ** Operations over double-precision floats *)
@@ -210,16 +217,16 @@ Definition eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2} := Beq_dec _ _.
 
 (** Arithmetic operations *)
 
-Definition neg: float -> float := Bopp _ _ neg_pl. (**r opposite (change sign) *)
-Definition abs: float -> float := Babs _ _ abs_pl. (**r absolute value (set sign to [+]) *)
+Definition neg: float -> float := Bopp _ _ neg_nan. (**r opposite (change sign) *)
+Definition abs: float -> float := Babs _ _ abs_nan. (**r absolute value (set sign to [+]) *)
 Definition add: float -> float -> float :=
-  Bplus 53 1024 __ __ binop_pl mode_NE. (**r addition *)
+  Bplus 53 1024 __ __ binop_nan mode_NE. (**r addition *)
 Definition sub: float -> float -> float :=
-  Bminus 53 1024 __ __ binop_pl mode_NE. (**r subtraction *)
+  Bminus 53 1024 __ __ binop_nan mode_NE. (**r subtraction *)
 Definition mul: float -> float -> float :=
-  Bmult 53 1024 __ __ binop_pl mode_NE. (**r multiplication *)
+  Bmult 53 1024 __ __ binop_nan mode_NE. (**r multiplication *)
 Definition div: float -> float -> float :=
-  Bdiv 53 1024 __ __ binop_pl mode_NE. (**r division *)
+  Bdiv 53 1024 __ __ binop_nan mode_NE. (**r division *)
 Definition compare (f1 f2: float) : option Datatypes.comparison := (**r general comparison *)
   Bcompare 53 1024 f1 f2.
 Definition cmp (c:comparison) (f1 f2: float) : bool := (**r Boolean comparison *)
@@ -229,8 +236,8 @@ Definition ordered (f1 f2: float) : bool :=
 
 (** Conversions *)
 
-Definition of_single: float32 -> float := Bconv _ _ 53 1024 __ __ of_single_pl mode_NE.
-Definition to_single: float -> float32 := Bconv _ _ 24 128 __ __ to_single_pl mode_NE.
+Definition of_single: float32 -> float := Bconv _ _ 53 1024 __ __ of_single_nan mode_NE.
+Definition to_single: float -> float32 := Bconv _ _ 24 128 __ __ to_single_nan mode_NE.
 
 Definition to_int (f:float): option int := (**r conversion to signed 32-bit int *)
   option_map Int.repr (ZofB_range _ _ f Int.min_signed Int.max_signed).
@@ -287,15 +294,19 @@ Ltac smart_omega :=
 Theorem add_commut:
   forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> add x y = add y x.
 Proof.
-  intros. apply Bplus_commut.
-  destruct x, y; try reflexivity. simpl in H. intuition congruence.
+  intros. apply Bplus_commut. unfold binop_nan.
+  destruct Archi.fpu_returns_default_qNaN. easy.
+  destruct x, y; try reflexivity.
+  now destruct H.
 Qed.
 
 Theorem mul_commut:
   forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> mul x y = mul y x.
 Proof.
-  intros. apply Bmult_commut.
-  destruct x, y; try reflexivity. simpl in H. intuition congruence.
+  intros. apply Bmult_commut. unfold binop_nan.
+  destruct Archi.fpu_returns_default_qNaN. easy.
+  destruct x, y; try reflexivity.
+  now destruct H.
 Qed.
 
 (** Multiplication by 2 is diagonal addition. *)
@@ -304,10 +315,10 @@ Theorem mul2_add:
   forall f, add f f = mul f (of_int (Int.repr 2%Z)).
 Proof.
   intros. apply Bmult2_Bplus.
-  intros. destruct x; try discriminate. simpl.
-  transitivity (b, transform_quiet_pl n).
-  destruct Archi.choose_binop_pl_64; auto.
-  destruct y; auto || discriminate.
+  intros x y Hx Hy. unfold binop_nan.
+  destruct Archi.fpu_returns_default_qNaN. easy.
+  destruct x as [| |sx px Nx|]; try discriminate.
+  now destruct y, Archi.choose_binop_pl_64.
 Qed.
 
 (** Divisions that can be turned into multiplication by an inverse. *)
@@ -317,11 +328,11 @@ Definition exact_inverse : float -> option float := Bexact_inverse 53 1024 __ __
 Theorem div_mul_inverse:
   forall x y z, exact_inverse y = Some z -> div x y = mul x z.
 Proof.
-  intros. apply Bdiv_mult_inverse; auto.
-  intros. destruct x0; try discriminate. simpl.
-  transitivity (b, transform_quiet_pl n).
-  destruct y0; reflexivity || discriminate.
-  destruct z0; reflexivity || discriminate.
+  intros. apply Bdiv_mult_inverse. 2: easy.
+  intros x0 y0 z0 Hx Hy Hz. unfold binop_nan.
+  destruct Archi.fpu_returns_default_qNaN. easy.
+  destruct x0 as [| |sx px Nx|]; try discriminate.
+  now destruct y0, z0.
 Qed.
 
 (** Properties of comparisons. *)
@@ -451,7 +462,7 @@ Proof.
   rewrite Bcompare_correct in CMP by auto.
   inv CMP. apply Rcompare_Lt_inv in H1. rewrite EQy in H1.
   assert (p < Int.unsigned ox8000_0000).
-  { apply lt_Z2R. eapply Rle_lt_trans; eauto. }
+  { apply lt_IZR. apply Rle_lt_trans with (1 := P) (2 := H1). }
   change Int.max_signed with (Int.unsigned ox8000_0000 - 1). omega.
 Qed.
 
@@ -471,7 +482,7 @@ Proof.
   intros (EQy & FINy & SIGNy).
   assert (FINx: is_finite _ _ x = true).
   { rewrite ZofB_correct in C. destruct (is_finite _ _ x) eqn:FINx; congruence. }
-  assert (GE: (B2R _ _ x >= Z2R (Int.unsigned ox8000_0000))%R).
+  assert (GE: (B2R _ _ x >= IZR (Int.unsigned ox8000_0000))%R).
   { rewrite <- EQy. unfold cmp, cmp_of_comparison, compare in H.
     rewrite Bcompare_correct in H by auto.
     destruct (Rcompare (B2R 53 1024 x) (B2R 53 1024 y)) eqn:CMP.
@@ -502,7 +513,6 @@ Proof.
   transitivity (split_bits 52 11 (join_bits 52 11 false (Int.unsigned x) 1075)).
   - f_equal. rewrite Int64.ofwords_add'. reflexivity.
   - apply split_join_bits.
-    compute; auto.
     generalize (Int.unsigned_range x).
     compute_this Int.modulus; compute_this (2^52); omega.
     compute_this (2^11); omega.
@@ -510,7 +520,7 @@ Qed.
 
 Lemma from_words_value:
   forall x,
-     B2R _ _ (from_words ox4330_0000 x) = (bpow radix2 52 + Z2R (Int.unsigned x))%R
+     B2R _ _ (from_words ox4330_0000 x) = (bpow radix2 52 + IZR (Int.unsigned x))%R
   /\ is_finite _ _ (from_words ox4330_0000 x) = true
   /\ Bsign _ _ (from_words ox4330_0000 x) = false.
 Proof.
@@ -520,7 +530,7 @@ Proof.
   destruct (Int.unsigned x + Z.pow_pos 2 52) eqn:?.
   exfalso; now smart_omega.
   simpl; rewrite <- Heqz;  unfold F2R; simpl. split; auto.
-  rewrite <- (Z2R_plus 4503599627370496), Rmult_1_r. f_equal. rewrite Z.add_comm. auto.
+  rewrite Rmult_1_r, plus_IZR. apply Rplus_comm.
   exfalso; now smart_omega.
 Qed.
 
@@ -533,7 +543,7 @@ Proof.
   destruct (BofZ_exact 53 1024 __ __ (2^52 + Int.unsigned x)) as (D & E & F).
   smart_omega.
   apply B2R_Bsign_inj; auto.
-  rewrite A, D. rewrite Z2R_plus. auto.
+  rewrite A, D. rewrite plus_IZR. auto.
   rewrite C, F. symmetry. apply Zlt_bool_false. smart_omega.
 Qed.
 
@@ -585,7 +595,6 @@ Proof.
   transitivity (split_bits 52 11 (join_bits 52 11 false (Int.unsigned x) 1107)).
   - f_equal. rewrite Int64.ofwords_add'. reflexivity.
   - apply split_join_bits.
-    compute; auto.
     generalize (Int.unsigned_range x).
     compute_this Int.modulus; compute_this (2^52); omega.
     compute_this (2^11); omega.
@@ -593,7 +602,7 @@ Qed.
 
 Lemma from_words_value':
   forall x,
-     B2R _ _ (from_words ox4530_0000 x) = (bpow radix2 84 + Z2R (Int.unsigned x * two_p 32))%R
+     B2R _ _ (from_words ox4530_0000 x) = (bpow radix2 84 + IZR (Int.unsigned x * two_p 32))%R
   /\ is_finite _ _ (from_words ox4530_0000 x) = true
   /\ Bsign _ _ (from_words ox4530_0000 x) = false.
 Proof.
@@ -603,8 +612,8 @@ Proof.
   destruct (Int.unsigned x + Z.pow_pos 2 52) eqn:?.
   exfalso; now smart_omega.
   simpl; rewrite <- Heqz;  unfold F2R; simpl. split; auto.
-  rewrite <- (Z2R_plus 19342813113834066795298816), <- (Z2R_mult _ 4294967296).
-  f_equal; compute_this (Z.pow_pos 2 52); compute_this (two_power_pos 32); ring.
+  rewrite plus_IZR, Rmult_plus_distr_r, <- 2!mult_IZR, Rplus_comm.
+  easy.
   assert (Zneg p < 0) by reflexivity.
   exfalso; now smart_omega.
 Qed.
@@ -620,7 +629,7 @@ Proof.
     with  ((2^52 + Int.unsigned x) * 2^32) by ring.
   apply integer_representable_n2p; auto. smart_omega. omega. omega.
   apply B2R_Bsign_inj; auto.
-  rewrite A, D. rewrite <- Z2R_Zpower by omega. rewrite <- Z2R_plus. auto.
+  rewrite A, D. rewrite <- IZR_Zpower by omega. rewrite <- plus_IZR. auto.
   rewrite C, F. symmetry. apply Zlt_bool_false.
   compute_this (2^84); compute_this (2^32); omega.
 Qed.
@@ -904,38 +913,45 @@ Module Float32.
 
 (** ** NaN payload manipulations *)
 
-Program Definition transform_quiet_pl (pl:nan_pl 24) : nan_pl 24 :=
-  Pos.lor pl (iter_nat xO 22 xH).
-Next Obligation.
-  destruct pl.
+Lemma transform_quiet_nan_proof (p : positive) :
+  nan_pl 24 p = true ->
+  nan_pl 24 (Pos.lor p (iter_nat xO 22 1%positive)) = true.
+Proof.
+  unfold nan_pl. intros K.
   simpl. rewrite Z.ltb_lt in *.
-  assert (forall x, Fcore_digits.digits2_pos x = Pos.size x).
-  { induction x0; simpl; auto; rewrite IHx0; zify; omega. }
+  assert (H : forall x, Digits.digits2_pos x = Pos.size x).
+  { induction x; simpl; auto; rewrite IHx; zify; omega. }
   rewrite H, Psize_log_inf, <- Zlog2_log_inf in *. clear H.
-  change (Z.pos (Pos.lor x 4194304)) with (Z.lor (Z.pos x) 4194304%Z).
+  change (Z.pos (Pos.lor p 4194304)) with (Z.lor (Z.pos p) 4194304%Z).
   rewrite Z.log2_lor by (zify; omega).
-  apply Z.max_case. auto. simpl. omega.
+  now apply Z.max_case.
 Qed.
 
-Lemma transform_quiet_pl_idempotent:
-  forall pl, transform_quiet_pl (transform_quiet_pl pl) = transform_quiet_pl pl.
-Proof.
-  intros []; simpl; intros. apply Float.nan_payload_fequal.
-  simpl. apply Float.lor_idempotent.
-Qed.
+Definition transform_quiet_nan s p H : {x : float32 | is_nan _ _ x = true} :=
+  exist _ (B754_nan 24 128 s _ (transform_quiet_nan_proof p H)) (eq_refl true).
 
-Definition neg_pl (s:bool) (pl:nan_pl 24) := (negb s, pl).
-Definition abs_pl (s:bool) (pl:nan_pl 24) := (false, pl).
+Definition neg_nan (f : float32) : { x : float32 | is_nan _ _ x = true } :=
+  match f with
+  | B754_nan s p H => exist _ (B754_nan 24 128 (negb s) p H) (eq_refl true)
+  | _ => Archi.default_nan_32
+  end.
+
+Definition abs_nan (f : float32) : { x : float32 | is_nan _ _ x = true } :=
+  match f with
+  | B754_nan s p H => exist _ (B754_nan 24 128 false p H) (eq_refl true)
+  | _ => Archi.default_nan_32
+  end.
 
-Definition binop_pl (x y: binary32) : bool*nan_pl 24 :=
+Definition binop_nan (x y : float32) : {x : float32 | is_nan _ _ x = true} :=
+  if Archi.fpu_returns_default_qNaN then Archi.default_nan_32 else
   match x, y with
-  | B754_nan s1 pl1, B754_nan s2 pl2 =>
-      if Archi.choose_binop_pl_32 s1 pl1 s2 pl2
-      then (s2, transform_quiet_pl pl2)
-      else (s1, transform_quiet_pl pl1)
-  | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1)
-  | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2)
-  | _, _ => Archi.default_pl_32
+  | B754_nan s1 pl1 H1, B754_nan s2 pl2 H2 =>
+      if Archi.choose_binop_pl_32 pl1 pl2
+      then transform_quiet_nan s2 pl2 H2
+      else transform_quiet_nan s1 pl1 H1
+  | B754_nan s1 pl1 H1, _ => transform_quiet_nan s1 pl1 H1
+  | _, B754_nan s2 pl2 H2 => transform_quiet_nan s2 pl2 H2
+  | _, _ => Archi.default_nan_32
   end.
 
 (** ** Operations over single-precision floats *)
@@ -946,16 +962,16 @@ Definition eq_dec: forall (f1 f2: float32), {f1 = f2} + {f1 <> f2} := Beq_dec _
 
 (** Arithmetic operations *)
 
-Definition neg: float32 -> float32 := Bopp _ _ neg_pl. (**r opposite (change sign) *)
-Definition abs: float32 -> float32 := Babs _ _ abs_pl. (**r absolute value (set sign to [+]) *)
+Definition neg: float32 -> float32 := Bopp _ _ neg_nan. (**r opposite (change sign) *)
+Definition abs: float32 -> float32 := Babs _ _ abs_nan. (**r absolute value (set sign to [+]) *)
 Definition add: float32 -> float32 -> float32 :=
-  Bplus 24 128 __ __ binop_pl mode_NE. (**r addition *)
+  Bplus 24 128 __ __ binop_nan mode_NE. (**r addition *)
 Definition sub: float32 -> float32 -> float32 :=
-  Bminus 24 128 __ __ binop_pl mode_NE. (**r subtraction *)
+  Bminus 24 128 __ __ binop_nan mode_NE. (**r subtraction *)
 Definition mul: float32 -> float32 -> float32 :=
-  Bmult 24 128 __ __ binop_pl mode_NE. (**r multiplication *)
+  Bmult 24 128 __ __ binop_nan mode_NE. (**r multiplication *)
 Definition div: float32 -> float32 -> float32 :=
-  Bdiv 24 128 __ __ binop_pl mode_NE. (**r division *)
+  Bdiv 24 128 __ __ binop_nan mode_NE. (**r division *)
 Definition compare (f1 f2: float32) : option Datatypes.comparison := (**r general comparison *)
   Bcompare 24 128 f1 f2.
 Definition cmp (c:comparison) (f1 f2: float32) : bool := (**r comparison *)
@@ -1003,15 +1019,19 @@ Definition of_bits (b: int): float32 := b32_of_bits (Int.unsigned b).
 Theorem add_commut:
   forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> add x y = add y x.
 Proof.
-  intros. apply Bplus_commut.
-  destruct x, y; try reflexivity. simpl in H. intuition congruence.
+  intros. apply Bplus_commut. unfold binop_nan.
+  destruct Archi.fpu_returns_default_qNaN. easy.
+  destruct x, y; try reflexivity.
+  now destruct H.
 Qed.
 
 Theorem mul_commut:
   forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> mul x y = mul y x.
 Proof.
-  intros. apply Bmult_commut.
-  destruct x, y; try reflexivity. simpl in H. intuition congruence.
+  intros. apply Bmult_commut. unfold binop_nan.
+  destruct Archi.fpu_returns_default_qNaN. easy.
+  destruct x, y; try reflexivity.
+  now destruct H.
 Qed.
 
 (** Multiplication by 2 is diagonal addition. *)
@@ -1020,10 +1040,10 @@ Theorem mul2_add:
   forall f, add f f = mul f (of_int (Int.repr 2%Z)).
 Proof.
   intros. apply Bmult2_Bplus.
-  intros. destruct x; try discriminate. simpl.
-  transitivity (b, transform_quiet_pl n).
-  destruct Archi.choose_binop_pl_32; auto.
-  destruct y; auto || discriminate.
+  intros x y Hx Hy. unfold binop_nan.
+  destruct Archi.fpu_returns_default_qNaN. easy.
+  destruct x as [| |sx px Nx|]; try discriminate.
+  now destruct y, Archi.choose_binop_pl_32.
 Qed.
 
 (** Divisions that can be turned into multiplication by an inverse. *)
@@ -1033,11 +1053,11 @@ Definition exact_inverse : float32 -> option float32 := Bexact_inverse 24 128 __
 Theorem div_mul_inverse:
   forall x y z, exact_inverse y = Some z -> div x y = mul x z.
 Proof.
-  intros. apply Bdiv_mult_inverse; auto.
-  intros. destruct x0; try discriminate. simpl.
-  transitivity (b, transform_quiet_pl n).
-  destruct y0; reflexivity || discriminate.
-  destruct z0; reflexivity || discriminate.
+  intros. apply Bdiv_mult_inverse. 2: easy.
+  intros x0 y0 z0 Hx Hy Hz. unfold binop_nan.
+  destruct Archi.fpu_returns_default_qNaN. easy.
+  destruct x0 as [| |sx px Nx|]; try discriminate.
+  now destruct y0, z0.
 Qed.
 
 (** Properties of comparisons. *)
@@ -1264,7 +1284,7 @@ Proof.
   intros.
   pose proof (Int64.unsigned_range n).
   unfold of_longu. erewrite of_long_round_odd.
-  unfold of_double, Float.to_single. instantiate (1 := Float.to_single_pl).
+  unfold of_double, Float.to_single. instantiate (1 := Float.to_single_nan).
   f_equal. unfold Float.of_longu. f_equal.
   set (n' := Z.land (Z.lor (Int64.unsigned n) (Z.land (Int64.unsigned n) 2047 + 2047)) (-2048)).
   assert (int_round_odd (Int64.unsigned n) 11 = n') by (apply int_round_odd_plus; omega).
@@ -1310,7 +1330,7 @@ Proof.
   intros.
   pose proof (Int64.signed_range n).
   unfold of_long. erewrite of_long_round_odd.
-  unfold of_double, Float.to_single. instantiate (1 := Float.to_single_pl).
+  unfold of_double, Float.to_single. instantiate (1 := Float.to_single_nan).
   f_equal. unfold Float.of_long. f_equal.
   set (n' := Z.land (Z.lor (Int64.signed n) (Z.land (Int64.signed n) 2047 + 2047)) (-2048)).
   assert (int_round_odd (Int64.signed n) 11 = n') by (apply int_round_odd_plus; omega).