From 46a5e479ad70b88ee8b640a61378d4aada499b0a Mon Sep 17 00:00:00 2001
From: Andrew Appel <appel@princeton.edu>
Date: Wed, 15 Jan 2025 07:16:49 -0500
Subject: [PATCH] Parameterize Nans by prec/emax rather than type

which makes the Nans class usable in other non-VCFLoat contexts.
---
 vcfloat/FPCompCert.v    | 181 +++++++++++++++++++---------------------
 vcfloat/FPCore.v        | 122 ++++++++++++++++-----------
 vcfloat/FPLang.v        |   8 +-
 vcfloat/FPLangOpt.v     |   8 +-
 vcfloat/FPLib.v         |   2 +-
 vcfloat/FPStdCompCert.v |   2 +-
 vcfloat/FPStdLib.v      | 133 ++++++++++++++++++-----------
 vcfloat/Float_lemmas.v  |  44 +++++-----
 vcfloat/Rounding.v      |  36 ++++----
 9 files changed, 295 insertions(+), 241 deletions(-)

diff --git a/vcfloat/FPCompCert.v b/vcfloat/FPCompCert.v
index 13161b4..b9076b6 100644
--- a/vcfloat/FPCompCert.v
+++ b/vcfloat/FPCompCert.v
@@ -29,15 +29,18 @@ Proof.
   apply ProofIrrelevance.ProofIrrelevanceTheory.EqdepTheory.inj_pair2 in H2; auto.
 Qed.
 
+Require Import Coq.Classes.EquivDec.
+Require Import ZArith.
 
 Lemma conv_nan_ex:
-  { conv_nan: forall ty1 ty2 (STD1: is_standard ty1) (STD2: is_standard ty2),
-                binary_float (fprec ty1) (femax ty1) -> (* guaranteed to be a nan, if this is not a nan then any result will do *)
-                nan_payload (fprec ty2) (femax ty2)
-  |
-  conv_nan Tsingle Tdouble _ _ = Floats.Float.of_single_nan
+  { conv_nan: forall (prec1 emax1 prec2 emax2 : Z),
+                (1< prec2)%Z ->
+                binary_float prec1 emax1 -> (* guaranteed to be a nan, if this is not a nan then any result will do *)
+                nan_payload prec2 emax2
+  | 
+  conv_nan (fprec Tsingle) (femax Tsingle) (fprec Tdouble) (femax Tdouble) (fprec_gt_one _) = Floats.Float.of_single_nan
   /\
-  conv_nan Tdouble Tsingle _ _ = Floats.Float.to_single_nan
+  conv_nan (fprec Tdouble) (femax Tdouble) (fprec Tsingle) (femax Tsingle) (fprec_gt_one _) =  Floats.Float.to_single_nan
   }.
 Proof.
   eapply exist.
@@ -45,27 +48,19 @@ Proof.
   {
     shelve.
   }
-  intros ty1 ty2 ? ?.
-  destruct (type_eq_dec ty1 Tsingle _ _).
-  {
-    subst.
-    destruct (type_eq_dec ty2 Tdouble _ _).
-    {
-      subst.
-      exact Floats.Float.of_single_nan.
-    }
-    auto using any_nan.
+  intros ? ? ? ? ?.
+(*  destruct (eq_dec (prec1, fprec Tsingle) (emax1, femax Tsingle)). *)
+  destruct (BinInt.Z.eq_dec prec1 (fprec Tsingle)). {
+    destruct (BinInt.Z.eq_dec emax1 (femax Tsingle)); [ | intros; auto using any_nan].
+    destruct (BinInt.Z.eq_dec prec2 (fprec Tdouble)); [ | intros; auto using any_nan].
+    destruct (BinInt.Z.eq_dec emax2 (femax Tdouble)); [ | intros; auto using any_nan].
+    subst; exact Floats.Float.of_single_nan.
   }
-  destruct (type_eq_dec ty1 Tdouble _ _).
-  {
-    subst.
-    destruct (type_eq_dec ty2 Tsingle _ _).
-    {
-      subst.
-      exact Floats.Float.to_single_nan.
-    }
-    intros.
-    auto using any_nan.
+  destruct (BinInt.Z.eq_dec prec1 (fprec Tdouble)). {
+    destruct (BinInt.Z.eq_dec emax1 (femax Tdouble)); [ | intros; auto using any_nan].
+    destruct (BinInt.Z.eq_dec prec2 (fprec Tsingle)); [ | intros; auto using any_nan].
+    destruct (BinInt.Z.eq_dec emax2 (femax Tsingle)); [ | intros; auto using any_nan].
+    subst; exact Floats.Float.to_single_nan.
   }
   intros.
   auto using any_nan.
@@ -75,14 +70,14 @@ Defined.
 
 Definition conv_nan := let (c, _) := conv_nan_ex in c.
 
-Lemma single_double_ex (U: _ -> Type):
-  (forall ty, U ty) ->
-  forall s: U Tsingle,
-  forall d: U Tdouble,
+Lemma single_double_ex (U: forall prec emax, (1<prec)%Z -> Type):
+  (forall prec emax H, U prec emax H) ->
+  forall (s: forall H, U (fprec Tsingle) (femax Tsingle) H)
+         (d: forall H, U (fprec Tdouble) (femax Tdouble) H),
     {
-      f: forall ty {STD: is_standard ty}, U ty |
-      f Tsingle _ = s /\
-      f Tdouble _ = d
+      f: forall prec emax H, U prec emax H |
+      f (fprec Tsingle) (femax Tsingle) = s /\
+      f (fprec Tdouble) (femax Tdouble) = d
     }.
 Proof.
   intro ref.
@@ -90,60 +85,59 @@ Proof.
   esplit.
   Unshelve.
   shelve.
-  intros ty ?.
-  destruct (type_eq_dec ty Tsingle _ _).
-  {
-    subst.
-    exact s.
+  intros prec emax H.
+  destruct (Z.eq_dec prec (fprec Tsingle)). {
+     destruct (Z.eq_dec emax (femax Tsingle)); [ | apply ref].
+     subst. apply s.
   }
-  destruct (type_eq_dec ty Tdouble _ _).
-  {
-    subst.
-    exact d.
+  destruct (Z.eq_dec prec (fprec Tdouble)). {
+     destruct (Z.eq_dec emax (femax Tdouble)); [ | apply ref].
+     subst. apply d.
   }
   apply ref.
   Unshelve.
   split; reflexivity.
 Defined.
 
-Definition single_double (U: _ -> Type)
-           (f_: forall ty, U ty)
-           (s: U Tsingle)
-           (d: U Tdouble)
+Definition single_double (U: forall prec emax, (1<prec)%Z -> Type)
+           (f_: forall prec emax H, U prec emax H)
+           (s: forall H, U (fprec Tsingle) (femax Tsingle) H)
+           (d: forall H, U (fprec Tdouble) (femax Tdouble) H)
 :
-  forall ty {STD: is_standard ty}, U ty :=
+  forall prec emax H, U prec emax H :=
   let (f, _) := single_double_ex U f_ s d in f.
 
-Definition binop_nan :  forall ty {STD: is_standard ty}, binary_float (fprec ty) (femax ty) ->
-       binary_float (fprec ty) (femax ty) ->
-       nan_payload (fprec ty) (femax ty) :=
+Definition binop_nan :  forall prec emax,
+       (1<prec)%Z ->
+       binary_float prec emax ->
+       binary_float prec emax ->
+       nan_payload prec emax :=
   single_double
-    (fun ty =>
-       binary_float (fprec ty) (femax ty) ->
-       binary_float (fprec ty) (femax ty) ->
-       nan_payload (fprec ty) (femax ty)) 
-     (fun ty  _ _ => any_nan ty)
-     Floats.Float32.binop_nan
-     Floats.Float.binop_nan.
+    (fun prec emax H =>
+       binary_float prec emax ->
+       binary_float prec emax ->
+       nan_payload prec emax) 
+     (fun prec emax H _ _ => any_nan prec emax H)
+     (fun _ => Floats.Float32.binop_nan)
+     (fun _ => Floats.Float.binop_nan).
 
 Definition abs_nan :=
   single_double
-    (fun ty =>
-       binary_float (fprec ty) (femax ty) ->
-       nan_payload (fprec ty) (femax ty)) 
-     (fun ty  _ => any_nan ty)
-     Floats.Float32.abs_nan
-     Floats.Float.abs_nan.
+    (fun prec emax H =>
+       binary_float prec emax ->
+       nan_payload prec emax) 
+     (fun prec emax H  _ => any_nan prec emax H)
+     (fun _ => Floats.Float32.abs_nan)
+     (fun _ => Floats.Float.abs_nan).
 
 Definition opp_nan :=
   single_double
-    (fun ty =>
-       binary_float (fprec ty) (femax ty) ->
-       nan_payload (fprec ty) (femax ty)) 
-     (fun ty  _ => any_nan ty)
-     Floats.Float32.neg_nan
-     Floats.Float.neg_nan.
-
+    (fun prec emax H =>
+       binary_float prec emax ->
+       nan_payload prec emax) 
+     (fun prec emax H  _ => any_nan prec emax H)
+     (fun _ => Floats.Float32.neg_nan)
+     (fun _ => Floats.Float.neg_nan).
 
 Module FMA_NAN. 
 (* some of these definitions adapted from [the open-source part of] CompCert  *)
@@ -151,24 +145,23 @@ Import ZArith. Import Coq.Lists.List.
 
 (** Transform a Nan payload to a quiet Nan payload. *)
 
-Definition quiet_nan_payload (t: type) (p: positive) :=
-  Z.to_pos (Zbits.P_mod_two_p (Pos.lor p ((Zaux.iter_nat xO (Z.to_nat (fprec t - 2)) 1%positive))) (Z.to_nat (fprec t - 1))).
+Definition quiet_nan_payload (prec: Z) (p: positive) :=
+  Z.to_pos (Zbits.P_mod_two_p (Pos.lor p ((Zaux.iter_nat xO (Z.to_nat (prec - 2)) 1%positive))) (Z.to_nat (prec - 1))).
 
-Lemma quiet_nan_proof (t: type): 
-   forall p, Binary.nan_pl (fprec t) (quiet_nan_payload t p) = true.
+Lemma quiet_nan_proof (prec: Z): (1<prec)%Z -> 
+   forall p, Binary.nan_pl prec (quiet_nan_payload prec p) = true.
 Proof. 
 intros.
-pose proof (fprec_gt_one t).
  apply normalized_nan; auto; lia.
 Qed.
 
-Definition quiet_nan (t: type) {STD: is_standard t} (sp: bool * positive) :
-         {x : binary_float (fprec t) (femax t) | Binary.is_nan _ _ x = true} :=
+Definition quiet_nan prec emax (H: (1<prec)%Z) (sp: bool * positive) :
+         {x : binary_float prec emax | Binary.is_nan _ _ x = true} :=
   let (s, p) := sp in
-  exist _ (Binary.B754_nan (fprec t) (femax t) s (quiet_nan_payload t p) 
-              (quiet_nan_proof t p)) (eq_refl _).
+  exist _ (Binary.B754_nan prec emax s (quiet_nan_payload prec p) 
+              (quiet_nan_proof prec H p)) (eq_refl _).
 
-Definition default_nan (t: type) := (fst Archi.default_nan_64, iter_nat (Z.to_nat (fprec t - 2)) _ xO xH).
+Definition default_nan (prec: Z) := (fst Archi.default_nan_64, iter_nat (Z.to_nat (prec - 2)) _ xO xH).
 
 Inductive NAN_SCHEME := NAN_SCHEME_ARM | NAN_SCHEME_X86 | NAN_SCHEME_RISCV.
 
@@ -196,33 +189,33 @@ Definition ARMchoose_nan (is_signaling: positive -> bool)
     end
   in choose_snan l0.
 
-Definition choose_nan (t: type) : list (bool * positive) -> bool * positive :=
+Definition choose_nan (prec: Z) : list (bool * positive) -> bool * positive :=
  match the_nan_scheme with
- | NAN_SCHEME_RISCV => fun _ => default_nan t
- | NAN_SCHEME_X86 => fun l => match l with nil => default_nan t | n :: _ => n end
- | NAN_SCHEME_ARM => ARMchoose_nan (fun p => negb (Pos.testbit p (Z.to_N (fprec t - 2))))
-                                          (default_nan t)
+ | NAN_SCHEME_RISCV => fun _ => default_nan prec
+ | NAN_SCHEME_X86 => fun l => match l with nil => default_nan prec | n :: _ => n end
+ | NAN_SCHEME_ARM => ARMchoose_nan (fun p => negb (Pos.testbit p (Z.to_N (prec - 2))))
+                                          (default_nan prec)
  end.
 
-Definition cons_pl {t: type} {STD: is_standard t} (x : binary_float (fprec t) (femax t)) (l : list (bool * positive)) :=
+Definition cons_pl {prec emax} (x : binary_float prec emax) (l : list (bool * positive)) :=
 match x with
 | Binary.B754_nan _ _ s p _ => (s, p) :: l
 | _ => l
 end.
 
-Definition fma_nan_1 (t: type) {STD: is_standard t} 
-    (x y z: binary_float (fprec t) (femax t)) : nan_payload (fprec t) (femax t) :=
+Definition fma_nan_1 prec emax H
+    (x y z: binary_float prec emax) : nan_payload prec emax :=
   let '(a, b, c) := Archi.fma_order x y z in
-  quiet_nan t (choose_nan t (cons_pl a (cons_pl b (cons_pl c nil)))).
+  quiet_nan prec emax H (choose_nan prec (cons_pl a (cons_pl b (cons_pl c nil)))).
 
-Definition fma_nan_pl (t: type) {STD: is_standard t} (x y z: binary_float (fprec t) (femax t)) : {x : binary_float (fprec t) (femax t) | Binary.is_nan _ _ x = true} :=
+Definition fma_nan_pl prec emax H (x y z: binary_float prec emax) : {x : binary_float prec emax | Binary.is_nan _ _ x = true} :=
   match x, y with
   | Binary.B754_infinity _ _ _, Binary.B754_zero _ _ _ | Binary.B754_zero _ _ _, Binary.B754_infinity _ _ _ =>
       if Archi.fma_invalid_mul_is_nan
-      then quiet_nan t (choose_nan t (default_nan t :: cons_pl z nil))
-      else fma_nan_1 t x y z
+      then quiet_nan prec emax H (choose_nan prec (default_nan prec :: cons_pl z nil))
+      else fma_nan_1 prec emax H x y z
   | _, _ =>
-      fma_nan_1 t x y z
+      fma_nan_1 prec emax H x y z
   end.
 
 End FMA_NAN.
@@ -235,7 +228,7 @@ End FMA_NAN.
     div_nan := binop_nan;
     abs_nan := abs_nan;
     opp_nan := opp_nan;
-    sqrt_nan := (fun ty _ _ => any_nan ty);
+    sqrt_nan := (fun prec emax H _ => any_nan prec emax H);
     fma_nan := FMA_NAN.fma_nan_pl
   }.
 
diff --git a/vcfloat/FPCore.v b/vcfloat/FPCore.v
index f0574a2..e1cd48c 100644
--- a/vcfloat/FPCore.v
+++ b/vcfloat/FPCore.v
@@ -301,49 +301,57 @@ Definition FT2R {t: type} : ftype t -> R :=
 
 Class Nans: Type :=
   {
-    conv_nan: forall ty1 ty2 {STD1: is_standard ty1} {STD2: is_standard ty2}, 
-                binary_float (fprec ty1) (femax ty1) -> (* guaranteed to be a nan, if this is not a nan then any result will do *)
-                nan_payload (fprec ty2) (femax ty2)
+    conv_nan: forall prec1 emax1 prec2 emax2,
+                (1<prec2)%Z ->
+                binary_float prec1 emax1 -> (* guaranteed to be a nan, if this is not a nan then any result will do *)
+                nan_payload prec2 emax2
     ;
     plus_nan:
-      forall ty {STD: is_standard ty},
-        binary_float (fprec ty) (femax ty) ->
-        binary_float (fprec ty) (femax ty) ->
-        nan_payload (fprec ty) (femax ty)
+      forall prec emax, 
+        (1<prec)%Z ->
+        binary_float prec emax ->
+        binary_float prec emax ->
+        nan_payload prec emax
     ;
     mult_nan:
-      forall ty {STD: is_standard ty},
-        binary_float (fprec ty) (femax ty) ->
-        binary_float (fprec ty) (femax ty) ->
-        nan_payload (fprec ty) (femax ty)
+      forall prec emax,
+        (1<prec)%Z ->
+        binary_float prec emax ->
+        binary_float prec emax ->
+        nan_payload prec emax
     ;
     div_nan:
-      forall ty {STD: is_standard ty},
-        binary_float (fprec ty) (femax ty) ->
-        binary_float (fprec ty) (femax ty) ->
-        nan_payload (fprec ty) (femax ty)
+      forall prec emax,
+        (1<prec)%Z ->
+        binary_float prec emax ->
+        binary_float prec emax ->
+        nan_payload prec emax
     ;
     abs_nan:
-      forall ty {STD: is_standard ty},
-        binary_float (fprec ty) (femax ty) -> (* guaranteed to be a nan, if this is not a nan then any result will do *)
-        nan_payload (fprec ty) (femax ty)
+      forall prec emax,
+        (1<prec)%Z ->
+        binary_float prec emax -> (* guaranteed to be a nan, if this is not a nan then any result will do *)
+        nan_payload prec emax
     ;
     opp_nan:
-      forall ty {STD: is_standard ty},
-        binary_float (fprec ty) (femax ty) -> (* guaranteed to be a nan, if this is not a nan then any result will do *)
-        nan_payload (fprec ty) (femax ty)
+      forall prec emax,
+        (1<prec)%Z ->
+        binary_float prec emax -> (* guaranteed to be a nan, if this is not a nan then any result will do *)
+        nan_payload prec emax
     ;
     sqrt_nan:
-      forall ty {STD: is_standard ty},
-        binary_float (fprec ty) (femax ty) ->
-        nan_payload (fprec ty) (femax ty)
+      forall prec emax,
+        (1<prec)%Z ->
+        binary_float prec emax ->
+        nan_payload prec emax
     ;
     fma_nan:
-      forall ty {STD: is_standard ty},
-        binary_float (fprec ty) (femax ty) ->
-        binary_float (fprec ty) (femax ty) ->
-        binary_float (fprec ty) (femax ty) ->
-        nan_payload (fprec ty) (femax ty)
+      forall prec emax,
+        (1<prec)%Z ->
+        binary_float prec emax ->
+        binary_float prec emax ->
+        binary_float prec emax ->
+        nan_payload prec emax
   }.
 
 Definition float_equiv {ty} (b1 b2: ftype ty) : Prop.
@@ -455,6 +463,19 @@ Proof.
   lia.
 Qed.
 
+
+Corollary any_nan prec emax: (1<prec)%Z -> nan_payload prec emax.
+Proof.
+ intro.
+ red.
+  assert (H0: Binary.nan_pl prec 1 = true).
+   unfold nan_pl. simpl. lia.
+  exists (Binary.B754_nan prec emax false 1 H0).
+  reflexivity.
+Defined.
+
+(*
+
 Corollary any_nan ty: nan_payload (fprec ty) (femax ty).
 Proof.
  red.
@@ -466,6 +487,7 @@ Proof.
   exists (Binary.B754_nan (fprec ty) (femax ty) false 1 H).
   reflexivity.
 Defined.
+*)
 
 Section WITHNANS.
 Context {NANS: Nans}.
@@ -487,7 +509,7 @@ destruct tto. destruct nonstd0; try contradiction. inversion H.
 destruct (nonstd tfrom) eqn:?H.
 destruct tfrom. destruct nonstd0; try contradiction. discriminate.
 apply (Bconv (fprec tfrom) (femax tfrom) (fprec tto) (femax tto)
-                        (fprec_gt_0 _) (fprec_lt_femax _) (conv_nan _ _) BinarySingleNaN.mode_NE f)
+                        (fprec_gt_0 _) (fprec_lt_femax _) (conv_nan _ _ _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE f)
 .
 Defined.
 
@@ -550,15 +572,15 @@ Qed.
 
 
 Definition BINOP (op: ltac:( let t := type of Bplus in exact t ) ) 
-      (op_nan: forall ty : type,
-       is_standard ty ->
-       binary_float (fprec ty) (femax ty) ->
-       binary_float (fprec ty) (femax ty) ->
-       nan_payload (fprec ty) (femax ty))
+      (op_nan: forall prec emax,
+       (1<prec) ->
+       binary_float prec emax ->
+       binary_float prec emax ->
+       nan_payload prec emax)
     ty `{STD: is_standard ty}
     (x y: ftype ty) : ftype ty := 
    ftype_of_float (op _ _ (fprec_gt_0 ty) (fprec_lt_femax ty) 
-                     (op_nan ty _) BinarySingleNaN.mode_NE
+                     (op_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE
             (float_of_ftype x) (float_of_ftype y)).
 
 Definition BPLUS := BINOP Bplus plus_nan.
@@ -567,17 +589,21 @@ Definition BMINUS := BINOP Bminus plus_nan. (* NOTE: must be same as the one use
 Definition BMULT := BINOP Bmult mult_nan.
 Definition BDIV := BINOP Bdiv div_nan.
 
-Definition UNOP (op: ltac:( let t := type of Bsqrt in exact t ) ) op_nan
+Definition UNOP (op: ltac:( let t := type of Bsqrt in exact t ) ) 
+   (op_nan: forall prec emax,
+       (1<prec) ->
+       binary_float prec emax ->
+       nan_payload prec emax)
     ty `{STD: is_standard ty}
       (x: ftype ty) : ftype ty := 
       ftype_of_float (op _ _ (fprec_gt_0 ty) (fprec_lt_femax ty) 
-                     (op_nan ty STD) BinarySingleNaN.mode_NE
+                     (op_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE
             (float_of_ftype x)).
 
 Definition BABS {ty} {STD: is_standard ty} (x: ftype ty) := 
-   ftype_of_float (Babs _ (femax ty) (abs_nan ty) (float_of_ftype x)).
+   ftype_of_float (Babs _ (femax ty) (abs_nan (fprec ty) (femax ty) (fprec_gt_one _)) (float_of_ftype x)).
 Definition BOPP {ty} {STD: is_standard ty} (x: ftype ty) :=
-   ftype_of_float (Bopp _ (femax ty) (opp_nan ty) (float_of_ftype x)).
+   ftype_of_float (Bopp _ (femax ty) (opp_nan (fprec ty) (femax ty) (fprec_gt_one _)) (float_of_ftype x)).
 
 Definition BSQRT :=  UNOP Bsqrt sqrt_nan.
 Arguments BSQRT {ty}.
@@ -644,22 +670,22 @@ repeat (match goal with
            const_float x1; const_float x2;
            change (@BDIV NANS t STD x1 x2) 
             with (Bdiv (fprec t) (femax t) (fprec_gt_0 t)
-              (fprec_lt_femax t) (div_nan t) BinarySingleNaN.mode_NE x1 x2)
+              (fprec_lt_femax t) (div_nan (fprec t) (femax t) (fprec_gt_one t)) BinarySingleNaN.mode_NE x1 x2)
 | |- context [@BMULT ?NANS ?t ?STD ?x1 ?x2] =>
            const_float x1; const_float x2;
            change (@BMULT NANS t STD x1 x2) 
              with (Bmult (fprec t) (femax t) (fprec_gt_0 t)
-                (fprec_lt_femax t) (mult_nan t) BinarySingleNaN.mode_NE x1 x2)
+                (fprec_lt_femax t) (mult_nan (fprec t) (femax t) (fprec_gt_one t)) BinarySingleNaN.mode_NE x1 x2)
 | |- context [@BPLUS ?NANS ?t ?STD ?x1 ?x2] =>
            const_float x1; const_float x2;
            change (@BPLUS NANS t STD x1 x2) 
            with (Bplus (fprec t) (femax t) (fprec_gt_0 t)
-                 (fprec_lt_femax t) (plus_nan t) BinarySingleNaN.mode_NE x1 x2)
+                 (fprec_lt_femax t) (plus_nan (fprec t) (femax t) (fprec_gt_one t)) BinarySingleNaN.mode_NE x1 x2)
 | |- context [@BMINUS ?NANS ?t ?STD ?x1 ?x2] =>
            const_float x1; const_float x2;
            change (@BMINUS NANS t STD x1 x2) 
            with (Bminus (fprec t) (femax t) (fprec_gt_0 t)
-              (fprec_lt_femax t) (plus_nan t) BinarySingleNaN.mode_NE x1 x2)
+                 (fprec_lt_femax t) (plus_nan (fprec t) (femax t) (fprec_gt_one t)) BinarySingleNaN.mode_NE x1 x2)
 | |- context [Bdiv ?prec ?emax ?a ?b ?c ?d ?x1 ?x2] =>
    const_float x1; const_float x2;
    tryif (const_Z prec; const_Z emax)
@@ -716,8 +742,8 @@ Definition Zconst (t: type) `{STD: is_standard t} (i: Z) : ftype t :=
 
 Lemma BPLUS_commut {NANS: Nans}: forall (t: type) `{STD: is_standard t} 
      (a b: ftype t), 
-    plus_nan t (float_of_ftype a) (float_of_ftype b) = 
-    plus_nan t (float_of_ftype b) (float_of_ftype a) -> 
+    plus_nan (fprec t) (femax t) (fprec_gt_one t) (float_of_ftype a) (float_of_ftype b) = 
+    plus_nan (fprec t) (femax t) (fprec_gt_one t) (float_of_ftype b) (float_of_ftype a) -> 
     BPLUS a b = BPLUS b a.
 Proof.
 intros. 
@@ -727,8 +753,8 @@ apply Bplus_commut; auto.
 Qed.
 
 Lemma BMULT_commut {NANS: Nans}: forall t `{STD: is_standard t} a b, 
-    mult_nan t (float_of_ftype a) (float_of_ftype b) = 
-    mult_nan t (float_of_ftype b) (float_of_ftype a) -> 
+    mult_nan (fprec t) (femax t) (fprec_gt_one t) (float_of_ftype a) (float_of_ftype b) = 
+    mult_nan (fprec t) (femax t) (fprec_gt_one t) (float_of_ftype b) (float_of_ftype a) -> 
     BMULT a b = BMULT b a.
 Proof.
 intros.
diff --git a/vcfloat/FPLang.v b/vcfloat/FPLang.v
index 052fc2e..486173d 100644
--- a/vcfloat/FPLang.v
+++ b/vcfloat/FPLang.v
@@ -412,7 +412,7 @@ destruct ltr.
     destruct x; try discriminate; simpl;
      rewrite ?Rmult_0_l, Rminus_0_r, Rabs_R0; lra.     
   +
-    assert (H2 := Bmult_correct_comm _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) x).
+    assert (H2 := Bmult_correct_comm _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) x).
     rewrite Rmult_comm in H2. 
     unfold BMULT, BINOP.
      rewrite !float_of_ftype_of_float.
@@ -438,7 +438,7 @@ destruct ltr.
     set (j := bpow radix2 _) in *. clearbody j.
     destruct x; try discriminate; simpl; rewrite ?Rmult_0_l, Rminus_0_r, Rabs_R0; lra.     
   +
-    assert (H2 := Bmult_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) x).
+    assert (H2 := Bmult_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) x).
     rewrite Rmult_comm in H2. 
     unfold BMULT, BINOP.
      rewrite !float_of_ftype_of_float.
@@ -473,7 +473,7 @@ destruct ltr; destruct  (Z_lt_le_dec ((Z.neg pow) + 1) (3 - femax ty));
   rewrite is_finite_Binary, !float_of_ftype_of_float.
 - rewrite (B2_zero _ _ l); unfold Bmult. destruct (float_of_ftype x); auto.
 - 
-    pose proof (Bmult_correct_comm _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) (float_of_ftype x)).
+    pose proof (Bmult_correct_comm _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) (float_of_ftype x)).
     rewrite Rmult_comm in H2. 
     pose proof (B2_correct ty (Z.neg pow) ltac:(lia)).
    rewrite H3 in H2.
@@ -485,7 +485,7 @@ destruct ltr; destruct  (Z_lt_le_dec ((Z.neg pow) + 1) (3 - femax ty));
    apply  InvShift_finite_aux; auto.
 - rewrite (B2_zero _ _ l); unfold Bmult. destruct (float_of_ftype x); auto.
 - 
-    pose proof (Bmult_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) (float_of_ftype x)).
+    pose proof (Bmult_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) (float_of_ftype x)).
     rewrite Rmult_comm in H2. 
     pose proof (B2_correct ty (Z.neg pow) ltac:(lia)).
    rewrite H3 in H2.
diff --git a/vcfloat/FPLangOpt.v b/vcfloat/FPLangOpt.v
index 33ab652..b4fcd1b 100644
--- a/vcfloat/FPLangOpt.v
+++ b/vcfloat/FPLangOpt.v
@@ -682,8 +682,8 @@ Local Lemma Bmult_div_inverse_equiv ty {STD: is_standard ty}:
   Binary.is_finite _ _ z = true ->
   Bexact_inverse (fprec ty) (femax ty) (fprec_gt_0 ty) (fprec_lt_femax ty) y = Some z -> 
   binary_float_equiv
-  (Binary.Bmult _ _ _ (fprec_lt_femax ty) (mult_nan ty) BinarySingleNaN.mode_NE x z) 
-  (Binary.Bdiv _ _ _ (fprec_lt_femax ty) (div_nan ty) BinarySingleNaN.mode_NE x y) .
+  (Binary.Bmult _ _ _ (fprec_lt_femax ty) (mult_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x z) 
+  (Binary.Bdiv _ _ _ (fprec_lt_femax ty) (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x y) .
 Proof. intros. apply binary_float_equiv_sym; apply Bdiv_mult_inverse_equiv; auto. Qed.
 
 Theorem Bmult_div_inverse_equiv2 ty {STD: is_standard ty}:
@@ -693,8 +693,8 @@ Theorem Bmult_div_inverse_equiv2 ty {STD: is_standard ty}:
   Binary.is_finite _ _ z = true ->
   Bexact_inverse (fprec ty) (femax ty) (fprec_gt_0 ty) (fprec_lt_femax ty) y = Some z -> 
   binary_float_equiv
-  (Binary.Bmult _ _ _ (fprec_lt_femax ty) (mult_nan ty) BinarySingleNaN.mode_NE x2 z)
-  (Binary.Bdiv _ _ _ (fprec_lt_femax ty) (div_nan ty) BinarySingleNaN.mode_NE x1 y) .
+  (Binary.Bmult _ _ _ (fprec_lt_femax ty) (mult_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x2 z)
+  (Binary.Bdiv _ _ _ (fprec_lt_femax ty) (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x1 y) .
 Proof. intros. apply binary_float_equiv_sym; apply Bdiv_mult_inverse_equiv2; auto. Qed.
 
 Lemma uncast_finite_strict:
diff --git a/vcfloat/FPLib.v b/vcfloat/FPLib.v
index 9dfc0dc..fc06648 100644
--- a/vcfloat/FPLib.v
+++ b/vcfloat/FPLib.v
@@ -6,7 +6,7 @@ Require Import Coq.Lists.List.
 Definition BFMA {NAN: Nans} {t: type} {STD: is_standard t} (x y z: ftype t) : ftype t :=
   ftype_of_float
     (Binary.Bfma (fprec t) (femax t) (fprec_gt_0 t)
-      (fprec_lt_femax t) (fma_nan t) BinarySingleNaN.mode_NE
+      (fprec_lt_femax t) (fma_nan (fprec t) (femax t) (fprec_gt_one _)) BinarySingleNaN.mode_NE
      (float_of_ftype x) (float_of_ftype y) (float_of_ftype z)).
 
 (* see https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/RelationPairs.20rewriting.20really.20slow *)
diff --git a/vcfloat/FPStdCompCert.v b/vcfloat/FPStdCompCert.v
index 7c0cca7..9df72b3 100644
--- a/vcfloat/FPStdCompCert.v
+++ b/vcfloat/FPStdCompCert.v
@@ -29,7 +29,7 @@ Qed.
 
 Require vcfloat.FPCompCert.
 
-#[export] Instance nans: Nans := FPCompCert.nans.
+#[export] Instance nans: FPCore.Nans := FPCompCert.nans.
 
 Lemma val_inject_eq_rect_r v ty1 e:
   val_inject v ty1 e ->
diff --git a/vcfloat/FPStdLib.v b/vcfloat/FPStdLib.v
index fbcbf3a..d33a862 100644
--- a/vcfloat/FPStdLib.v
+++ b/vcfloat/FPStdLib.v
@@ -132,54 +132,71 @@ Proof.
 intros. apply I.
 Qed.
 
-
+(*
 Definition Nans := FPCore.Nans.
+*)
+(*
 Existing Class Nans.
 
 Definition conv_nan {NAN: Nans} : forall ty1 ty2 : type, 
                 binary_float (fprec ty1) (femax ty1) ->
                 nan_payload (fprec ty2) (femax ty2) 
-  := fun t1 t2 => @FPCore.conv_nan NAN (coretype_of_type t1) (coretype_of_type t2) _ _.
+  := fun t1 t2 => @FPCore.conv_nan NAN 
+        (FPCore.fprec (coretype_of_type t1))
+        (FPCore.femax (coretype_of_type t1))
+        (FPCore.fprec (coretype_of_type t2))
+        (FPCore.femax (coretype_of_type t2)) (FPCore.fprec_gt_one (coretype_of_type t2)).
 
 Definition plus_nan {NAN: Nans}:
       forall ty: type,
         binary_float (fprec ty) (femax ty) ->
         binary_float (fprec ty) (femax ty) ->
         nan_payload (fprec ty) (femax ty) 
- := fun t => @FPCore.plus_nan NAN (coretype_of_type t) _.
+ := fun t => @FPCore.plus_nan NAN 
+        (FPCore.fprec (coretype_of_type t))
+        (FPCore.femax (coretype_of_type t)) (FPCore.fprec_gt_one (coretype_of_type t)).
 
 Definition  mult_nan {NAN: Nans}:
       forall ty : type,
         binary_float (fprec ty) (femax ty) ->
         binary_float (fprec ty) (femax ty) ->
         nan_payload (fprec ty) (femax ty)
- := fun t => @FPCore.plus_nan NAN (coretype_of_type t) _.
-
+ := fun t => @FPCore.plus_nan NAN 
+        (FPCore.fprec (coretype_of_type t))
+        (FPCore.femax (coretype_of_type t)) (FPCore.fprec_gt_one (coretype_of_type t)).
 
 Definition    div_nan {NAN: Nans}:
       forall ty : type,
         binary_float (fprec ty) (femax ty) ->
         binary_float (fprec ty) (femax ty) ->
         nan_payload (fprec ty) (femax ty)
- := fun t => @FPCore.div_nan NAN (coretype_of_type t) _.
+ := fun t => @FPCore.div_nan NAN 
+        (FPCore.fprec (coretype_of_type t))
+        (FPCore.femax (coretype_of_type t)) (FPCore.fprec_gt_one (coretype_of_type t)).
 
 Definition    abs_nan {NAN: Nans}:
       forall ty : type,
         binary_float (fprec ty) (femax ty) -> (* guaranteed to be a nan, if this is not a nan then any result will do *)
         nan_payload (fprec ty) (femax ty)
- := fun t => @FPCore.abs_nan NAN (coretype_of_type t) _.
+ := fun t => @FPCore.abs_nan NAN 
+        (FPCore.fprec (coretype_of_type t))
+        (FPCore.femax (coretype_of_type t)) (FPCore.fprec_gt_one (coretype_of_type t)).
 
 Definition    opp_nan {NAN: Nans}:
       forall ty : type,
         binary_float (fprec ty) (femax ty) -> (* guaranteed to be a nan, if this is not a nan then any result will do *)
         nan_payload (fprec ty) (femax ty)
- := fun t => @FPCore.opp_nan NAN (coretype_of_type t) _.
+ := fun t => @FPCore.opp_nan NAN 
+        (FPCore.fprec (coretype_of_type t))
+        (FPCore.femax (coretype_of_type t)) (FPCore.fprec_gt_one (coretype_of_type t)).
 
 Definition    sqrt_nan {NAN: Nans}:
       forall ty : type,
         binary_float (fprec ty) (femax ty) ->
         nan_payload (fprec ty) (femax ty)
- := fun t => @FPCore.sqrt_nan NAN (coretype_of_type t) _.
+ := fun t => @FPCore.sqrt_nan NAN 
+        (FPCore.fprec (coretype_of_type t))
+        (FPCore.femax (coretype_of_type t)) (FPCore.fprec_gt_one (coretype_of_type t)).
 
 Definition    fma_nan {NAN: Nans}:
       forall ty : type,
@@ -187,7 +204,11 @@ Definition    fma_nan {NAN: Nans}:
         binary_float (fprec ty) (femax ty) ->
         binary_float (fprec ty) (femax ty) ->
         nan_payload (fprec ty) (femax ty)
- := fun t => @FPCore.fma_nan NAN (coretype_of_type t) _.
+ := fun t => @FPCore.fma_nan NAN 
+        (FPCore.fprec (coretype_of_type t))
+        (FPCore.femax (coretype_of_type t)) (FPCore.fprec_gt_one (coretype_of_type t)).
+
+*)
 
 Lemma fprec_gt_one ty:
   (1 < fprec ty)%Z.
@@ -202,6 +223,7 @@ Proof.
   lia.
 Qed.
 
+(*
 
 Corollary any_nan ty: nan_payload (fprec ty) (femax ty).
 Proof.
@@ -214,13 +236,13 @@ Proof.
   exists (Binary.B754_nan (fprec ty) (femax ty) false 1 H).
   reflexivity.
 Defined.
-
+*)
 
 Definition FT2R {t: type} : ftype t -> R := B2R (fprec t) (femax t).
 
-Definition BFMA {NAN: Nans} {t: type} : forall (x y z: ftype t), ftype t :=
+Definition BFMA {NAN: FPCore.Nans} {t: type} : forall (x y z: ftype t), ftype t :=
     Binary.Bfma (fprec t) (femax t) (fprec_gt_0 t)
-      (fprec_lt_femax t) (fma_nan t) BinarySingleNaN.mode_NE.
+      (fprec_lt_femax t) (FPCore.fma_nan (fprec t) (femax t) (fprec_gt_one t)) BinarySingleNaN.mode_NE.
 
 (* see https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/RelationPairs.20rewriting.20really.20slow *)
 Global Instance proper_pair1: forall A B RA1 RA2 RB1 RB2 (RA : relation A) (RB : relation B),
@@ -387,7 +409,7 @@ Add Parametric Relation {t: type}: (ftype t) (@strict_feq t)
  (* See https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/rewriting.20with.20PERs *)
     (lazymatch R with respectful _ _ => fail | _ => red; auto with nocore typeclass_instances end)    : typeclass_instances.
 
-Add Parametric Morphism {NAN: Nans}{t: type} : BFMA
+Add Parametric Morphism {NAN: FPCore.Nans}{t: type} : BFMA
  with signature (@feq t) ==> feq ==> feq ==> feq
   as BFMA_mor.
 Proof.
@@ -451,37 +473,46 @@ Definition adapt_unop_nan
 *)
   
 Definition BINOP (op: ltac:( let t := type of Bplus in exact t ) ) 
-   (op_nan: forall ty : type,
-       binary_float (fprec ty) (femax ty) ->
-       binary_float (fprec ty) (femax ty) ->
-       nan_payload (fprec ty) (femax ty))
+   (op_nan: forall prec emax,
+       (1<prec)%Z ->
+       binary_float prec emax ->
+       binary_float prec emax ->
+       nan_payload prec emax)
     ty 
     : ftype ty -> ftype ty -> ftype ty 
-    := op _ _ (fprec_gt_0 ty) (fprec_lt_femax ty) (op_nan ty)
+    := op _ _ (fprec_gt_0 ty) (fprec_lt_femax ty) (op_nan (fprec ty) (femax ty) (fprec_gt_one ty))
       BinarySingleNaN.mode_NE.
 
 Section WITHNANS.
-Context {NANS: Nans}.
+Context {NANS: FPCore.Nans}.
+
+Definition BPLUS := BINOP Bplus FPCore.plus_nan.
+Definition BMINUS := BINOP Bminus FPCore.plus_nan. (* NOTE: must be same as the one used for plus *)
 
-Definition BPLUS := BINOP Bplus plus_nan.
-Definition BMINUS := BINOP Bminus plus_nan. (* NOTE: must be same as the one used for plus *)
+Definition BMULT := BINOP Bmult FPCore.mult_nan.
+Definition BABS {ty} := Babs _ (femax ty) (FPCore.abs_nan (fprec ty) (femax ty) (fprec_gt_one ty)).
+Definition BDIV := BINOP Bdiv FPCore.div_nan.
+Definition BOPP {ty} := Bopp _ (femax ty) (FPCore.opp_nan (fprec ty) (femax ty) (fprec_gt_one ty)).
 
-Definition BMULT := BINOP Bmult mult_nan.
-Definition BDIV := BINOP Bdiv div_nan.
-Definition BABS {ty} := Babs _ (femax ty) (abs_nan ty).
-Definition BOPP {ty} := Bopp _ (femax ty) (opp_nan ty).
+Definition UNOP (op: ltac:( let t := type of Bsqrt in exact t ) ) 
 
-Definition UNOP (op: ltac:( let t := type of Bsqrt in exact t ) ) op_nan ty 
+   (op_nan: forall prec emax,
+       (1<prec)%Z ->
+       binary_float prec emax ->
+       nan_payload prec emax)
+      ty 
     : ftype ty -> ftype ty
-    := op _ _ (fprec_gt_0 ty) (fprec_lt_femax ty) (op_nan ty) BinarySingleNaN.mode_NE.
+    := op (fprec ty) (femax ty) (fprec_gt_0 ty) (fprec_lt_femax ty) (op_nan (fprec ty) (femax ty) (fprec_gt_one ty)) 
+                BinarySingleNaN.mode_NE.
 
-Definition BSQRT :=  UNOP Bsqrt sqrt_nan.
+Definition BSQRT :=  UNOP Bsqrt FPCore.sqrt_nan.
 
 Definition cast (tto: type) {tfrom: type} (f: ftype tfrom): ftype tto :=
   match type_eq_dec tfrom tto with
     | left r => eq_rect _ _ f _ r
     | _ => Bconv (fprec tfrom) (femax tfrom) (fprec tto) (femax tto)
-                        (fprec_gt_0 _) (fprec_lt_femax _) (conv_nan _ _) BinarySingleNaN.mode_NE f
+                        (fprec_gt_0 _) (fprec_lt_femax _) 
+                 (FPCore.conv_nan  (fprec tfrom) (femax tfrom) (fprec tto) (femax tto) (fprec_gt_one tto)) BinarySingleNaN.mode_NE f
   end.
 
 End WITHNANS.
@@ -534,7 +565,7 @@ Definition Zconst (t: type) (i: Z) : ftype t :=
     BofZ (fprec t) (femax t) (Pos2Z.is_pos (fprecp t)) (fprec_lt_femax t) i.
 
 Lemma BPLUS_BOPP_diag: 
-  forall {NAN: Nans} {t} (x: ftype t), finite x -> BPLUS x (BOPP x) = Zconst t 0.
+  forall {NAN: FPCore.Nans} {t} (x: ftype t), finite x -> BPLUS x (BOPP x) = Zconst t 0.
 Proof.
 intros.
 destruct x,s; inv H; try reflexivity;
@@ -557,7 +588,7 @@ inv H.
 constructor; auto.
 Qed.
 
-Lemma BFMA_zero1: forall {NAN: Nans} {t} y s, 
+Lemma BFMA_zero1: forall {NAN: FPCore.Nans} {t} y s, 
   strict_feq y y ->
   feq (BFMA (Zconst t 0) y s) s.
 Proof.
@@ -569,7 +600,7 @@ unfold BFMA, BPLUS, BINOP in *.
 destruct y, s; try discriminate; simpl; auto.
 Qed.
 
-Lemma BFMA_zero2: forall  {NAN: Nans}{t} x s, 
+Lemma BFMA_zero2: forall  {NAN: FPCore.Nans}{t} x s, 
   strict_feq x x ->
   feq (BFMA x (Zconst t 0) s) s.
 Proof.
@@ -581,14 +612,14 @@ unfold BFMA, BPLUS, BINOP in *.
 destruct x, s; try discriminate; simpl; auto.
 Qed.
 
-Lemma BPLUS_0_l: forall  {NAN: Nans} {t} x, finite x -> 
+Lemma BPLUS_0_l: forall  {NAN: FPCore.Nans} {t} x, finite x -> 
       feq (BPLUS (Zconst t 0) x) x.
 Proof.
   intros. destruct x; try contradiction;
  destruct s; simpl; auto.
 Qed.
 
-Lemma BPLUS_0_r: forall {NAN: Nans} {t} x, finite x -> 
+Lemma BPLUS_0_r: forall {NAN: FPCore.Nans} {t} x, finite x -> 
       feq (BPLUS x (Zconst t 0)) x.
 Proof.
   intros. destruct x; try contradiction;
@@ -601,7 +632,7 @@ intros; apply I.
 Qed.
 
 Lemma BMULT_congr:
- forall  {NAN: Nans}{t} (x x' y y': ftype t), feq x x' -> feq y y' -> 
+ forall  {NAN: FPCore.Nans}{t} (x x' y y': ftype t), feq x x' -> feq y y' -> 
    feq (BMULT x y) (BMULT x' y').
 Proof.
 intros.
@@ -612,7 +643,7 @@ apply feq_refl.
 Qed.
 
 Lemma BMINUS_congr:
- forall  {NAN: Nans}{t} (x x' y y': ftype t), feq x x' -> feq y y' -> 
+ forall  {NAN: FPCore.Nans}{t} (x x' y y': ftype t), feq x x' -> feq y y' -> 
    feq (BMINUS x y) (BMINUS x' y').
 Proof.
 intros.
@@ -652,7 +683,7 @@ Qed.
 #[export] Hint Resolve Forall2_subrelation: core.
 
 Lemma BFMA_xx_mor:
- forall  {NAN: Nans}{t} (x x' s s': ftype t), 
+ forall  {NAN: FPCore.Nans}{t} (x x' s s': ftype t), 
   feq x x' -> 
   feq s s' ->
   feq (BFMA x x s) (BFMA x' x' s').
@@ -686,7 +717,7 @@ Proof.
  destruct y; inv H0. constructor. constructor; auto.
 Qed.
 
-Lemma FMA_one: forall {NAN: Nans}{t} (x y: ftype t),
+Lemma FMA_one: forall {NAN: FPCore.Nans}{t} (x y: ftype t),
   feq (BFMA x y (Zconst t 0)) (BMULT x y).
 Proof.
 unfold BFMA, BMULT, BINOP.
@@ -739,7 +770,7 @@ intros.
 destruct x,y; inv H; constructor; auto.
 Qed.
 
-Lemma BFMA_finite_e {NAN: Nans} {t: type}:
+Lemma BFMA_finite_e {NAN: FPCore.Nans} {t: type}:
  forall x y z : ftype t,
  finite (BFMA x y z) ->
  finite x /\ finite y /\ finite z.
@@ -777,7 +808,7 @@ rewrite <- H; auto. apply IHForall2; auto. rewrite H; auto.
 apply IHForall2; auto.
 Qed.
 
-Add Parametric Morphism {NAN: Nans}{t}: (@BPLUS NAN t)
+Add Parametric Morphism {NAN: FPCore.Nans}{t}: (@BPLUS NAN t)
  with signature feq ==> feq ==> feq
  as BPLUS_mor.
 Proof.
@@ -790,7 +821,7 @@ repeat proof_irr;
 try constructor; auto.
 Qed.
 
-Add Parametric Morphism {NAN: Nans}{t}: (@BMINUS NAN t)
+Add Parametric Morphism {NAN: FPCore.Nans}{t}: (@BMINUS NAN t)
  with signature feq ==> feq ==> feq
  as BMINUS_mor.
 Proof.
@@ -803,7 +834,7 @@ repeat proof_irr;
 try constructor; auto.
 Qed.
 
-Add Parametric Morphism {NAN: Nans}{t}: (@BMULT NAN t)
+Add Parametric Morphism {NAN: FPCore.Nans}{t}: (@BMULT NAN t)
  with signature feq ==> feq ==> feq
  as BMULT_mor.
 Proof.
@@ -816,7 +847,7 @@ repeat proof_irr;
 try constructor; auto.
 Qed.
 
-Add Parametric Morphism {NAN: Nans}{t}: (@BDIV NAN t)
+Add Parametric Morphism {NAN: FPCore.Nans}{t}: (@BDIV NAN t)
  with signature feq ==> strict_feq ==> feq
  as BDIV_mor.
 Proof.
@@ -884,10 +915,10 @@ Inductive type_coretype: forall [t: type], ftype t -> FPCore.ftype (coretype_of_
       type_coretype (@Zconst t z) (@FPCore.Zconst (coretype_of_type t) (STDtype t) z)
 | TC_BINOP: forall op NAN t 
         x x' (TCx: type_coretype x x') y y' (TCy: type_coretype y y'),
-        type_coretype (@BINOP op NAN t x y) (@FPCore.BINOP op (coreNAN2 NAN) (coretype_of_type t) (STDtype t) x' y')
+        type_coretype (@BINOP op NAN t x y) (@FPCore.BINOP op NAN (coretype_of_type t) (STDtype t) x' y')
 | TC_UNOP: forall op NAN t x x',
         type_coretype x x' ->
-        type_coretype (@UNOP op NAN t x) (@FPCore.UNOP op (coreNAN1 NAN) (coretype_of_type t) (STDtype t) x')
+        type_coretype (@UNOP op NAN t x) (@FPCore.UNOP op NAN (coretype_of_type t) (STDtype t) x')
 | TC_cast: forall NAN t1 t2  x x',
       type_coretype  x x' ->
       type_coretype (@cast NAN t1 t2 x) 
@@ -939,6 +970,7 @@ unfold coretype_of_type, type_of_coretype;
 destruct t; simpl.
 replace (ZLT_intro _ _ _) with (fprec_lt_femax_bool0) by apply proof_irr.
 auto.
+f_equal. apply proof_irr.
 apply JMeq_eq; auto.
 apply JMeq_eq; auto.
 -
@@ -951,6 +983,7 @@ unfold coretype_of_type, type_of_coretype;
 destruct t; simpl.
 replace (ZLT_intro _ _ _) with (fprec_lt_femax_bool0) by apply proof_irr.
 auto.
+f_equal. apply proof_irr.
 apply JMeq_eq; auto.
 -
 unfold cast, FPCore.cast.
@@ -983,14 +1016,16 @@ destruct (FPCore.type_eq_dec _ _ _ _).
   unfold coretype_of_type in *.
   simpl in *. clear H.
   f_equal. apply proof_irr.
+  simpl.
+  f_equal. apply proof_irr.
 Qed. 
 
 Module Test.
 
-Definition foo {Nans: Nans} (x: ftype Tsingle) :=
+Definition foo {Nans: FPCore.Nans} (x: ftype Tsingle) :=
    BPLUS (cast Tdouble x) (Zconst Tdouble 8).
 
-Definition foo' {Nans: Nans} (x: FPCore.ftype FPCore.Tsingle) :=
+Definition foo' {Nans: FPCore.Nans} (x: FPCore.ftype FPCore.Tsingle) :=
    @FPCore.BPLUS Nans _ FPCore.is_standard_Tdouble 
       (@FPCore.cast Nans _ _ FPCore.is_standard_Tdouble FPCore.is_standard_Tsingle x)
       (@FPCore.Zconst FPCore.Tdouble FPCore.is_standard_Tdouble 8).
@@ -1004,7 +1039,7 @@ Proof.
 Qed.
 
 
-Definition corify {NAN: Nans} (x: ftype Tsingle) (x': FPCore.ftype FPCore.Tsingle):
+Definition corify {NAN: FPCore.Nans} (x: ftype Tsingle) (x': FPCore.ftype FPCore.Tsingle):
    type_coretype x x' ->
    {e' : FPCore.ftype FPCore.Tdouble | JMeq (foo x) e'}.
 Proof.
diff --git a/vcfloat/Float_lemmas.v b/vcfloat/Float_lemmas.v
index edde204..44e5ffd 100644
--- a/vcfloat/Float_lemmas.v
+++ b/vcfloat/Float_lemmas.v
@@ -31,7 +31,7 @@ Section WITHNANS.
 
 Context {NANS: Nans}.
 
-Definition Bsqrt ty {STD: is_standard ty}:= Bsqrt _ _ (fprec_gt_0 ty) (fprec_lt_femax ty) (sqrt_nan ty) BinarySingleNaN.mode_NE.
+Definition Bsqrt ty {STD: is_standard ty}:= Bsqrt _ _ (fprec_gt_0 ty) (fprec_lt_femax ty) (sqrt_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE.
 
 Definition F2 prec emax e  :=
 if Z_lt_le_dec (e+1) (3 - emax)
@@ -368,15 +368,15 @@ Theorem Bdiv_mult_inverse_finite ty {STD: is_standard ty} :
   Binary.is_finite _ _ y = true ->
   Binary.is_finite _ _ z = true ->
   Bexact_inverse (fprec ty) (femax ty) (fprec_gt_0 ty) (fprec_lt_femax ty) y = Some z -> 
-  Bdiv _ _ _ (fprec_lt_femax ty) (div_nan ty) BinarySingleNaN.mode_NE x y =
-  Bmult _ _ _ (fprec_lt_femax ty) (mult_nan ty) BinarySingleNaN.mode_NE x z .
+  Bdiv _ _ _ (fprec_lt_femax ty) (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x y =
+  Bmult _ _ _ (fprec_lt_femax ty) (mult_nan  (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x z .
 Proof.
   intros.
   destruct (Bexact_inverse_correct _ _ _ _ _ _ H2) as (A & B & C & D & E).
   assert (HMUL :=Binary.Bmult_correct (fprec ty)  (femax ty) 
-                     (fprec_gt_0 ty) (fprec_lt_femax ty) (mult_nan ty) BinarySingleNaN.mode_NE x z).
+                     (fprec_gt_0 ty) (fprec_lt_femax ty) (mult_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x z).
   assert (HDIV := Binary.Bdiv_correct  (fprec ty)  (femax ty)  
-                    (fprec_gt_0 ty) (fprec_lt_femax ty) (div_nan ty) BinarySingleNaN.mode_NE x y D).
+                    (fprec_gt_0 ty) (fprec_lt_femax ty) (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x y D).
  unfold Rdiv in HDIV.
  rewrite <- C in HDIV.
  destruct Rlt_bool.
@@ -385,20 +385,20 @@ Proof.
   destruct HDIV as (S & T & U).
   assert (Binary.is_finite  (fprec ty) (femax ty)
                (Binary.Bmult (fprec ty) (femax ty)  (fprec_gt_0 ty) (fprec_lt_femax ty) 
-                   (mult_nan ty) BinarySingleNaN.mode_NE x z) = true) 
+                   (mult_nan  (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x z) = true) 
    by  (rewrite Q; auto;  rewrite ?andb_true_iff; auto).
   assert (Binary.is_finite (fprec ty) (femax ty)
               (Binary.Bdiv (fprec ty) (femax ty)  (fprec_gt_0 ty) (fprec_lt_femax ty) 
-                   (div_nan ty) BinarySingleNaN.mode_NE x y) = true)
+                   (div_nan  (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x y) = true)
     by (rewrite T; auto).
   apply Binary.B2R_Bsign_inj; auto;
   rewrite ?S, ?R, ?U, ?E; auto; apply is_finite_not_is_nan; auto.
 - 
   pose proof Binary.B2FF_inj _ _
        (Binary.Bdiv (fprec ty) (femax ty) (fprec_gt_0 ty) 
-            (fprec_lt_femax ty) (div_nan ty) BinarySingleNaN.mode_NE x y)
+            (fprec_lt_femax ty) (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x y)
       (Binary.Bmult (fprec ty) (femax ty) (fprec_gt_0 ty) 
-            (fprec_lt_femax ty) (mult_nan ty) BinarySingleNaN.mode_NE x z).
+            (fprec_lt_femax ty) (mult_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x z).
   rewrite E in HMUL.
   rewrite HMUL, HDIV in *; auto.
 Qed.
@@ -409,15 +409,15 @@ Theorem Bdiv_mult_inverse_nan ty {STD: is_standard ty}:
   Binary.is_finite _ _ y = true ->
   Binary.is_finite _ _ z = true ->
   Bexact_inverse (fprec ty) (femax ty) (fprec_gt_0 ty) (fprec_lt_femax ty) y = Some z -> 
-  Bdiv _ _ _ (fprec_lt_femax ty) (div_nan ty) BinarySingleNaN.mode_NE x y =
-  Bmult _ _ _ (fprec_lt_femax ty) (mult_nan ty) BinarySingleNaN.mode_NE x z .
+  Bdiv _ _ _ (fprec_lt_femax ty) (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x y =
+  Bmult _ _ _ (fprec_lt_femax ty) (mult_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x z .
 Proof.
   intros.
   destruct (Bexact_inverse_correct _ _ _ _ _ _ H2) as (A & B & C & D & E).
   assert (HMUL :=Binary.Bmult_correct (fprec ty)  (femax ty) 
-                     (fprec_gt_0 ty) (fprec_lt_femax ty) (mult_nan ty) BinarySingleNaN.mode_NE x z).
+                     (fprec_gt_0 ty) (fprec_lt_femax ty) (mult_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x z).
   assert (HDIV := Binary.Bdiv_correct  (fprec ty)  (femax ty)  
-                    (fprec_gt_0 ty) (fprec_lt_femax ty) (div_nan ty) BinarySingleNaN.mode_NE x y D).
+                    (fprec_gt_0 ty) (fprec_lt_femax ty) (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x y D).
  unfold Rdiv in HDIV.
  rewrite <- C in HDIV.
  destruct Rlt_bool.
@@ -429,11 +429,11 @@ Proof.
  set (x:= (B754_zero (fprec ty) (femax ty) s)) in *.
  assert (Binary.is_finite  (fprec ty) (femax ty)
                (Binary.Bmult (fprec ty) (femax ty)  (fprec_gt_0 ty) (fprec_lt_femax ty) 
-                   (mult_nan ty) BinarySingleNaN.mode_NE x z) = true) 
+                   (mult_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x z) = true) 
    by  (rewrite Q; auto;  rewrite ?andb_true_iff; auto).
   assert (Binary.is_finite (fprec ty) (femax ty)
               (Binary.Bdiv (fprec ty) (femax ty)  (fprec_gt_0 ty) (fprec_lt_femax ty) 
-                   (div_nan ty) BinarySingleNaN.mode_NE x y) = true)
+                   (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x y) = true)
     by (rewrite T; auto).
   apply Binary.B2R_Bsign_inj; auto;
   rewrite ?S, ?R, ?U, ?E; auto; apply is_finite_not_is_nan; auto.
@@ -445,9 +445,9 @@ Proof.
 - 
   pose proof Binary.B2FF_inj _ _
        (Binary.Bdiv (fprec ty) (femax ty) (fprec_gt_0 ty) 
-            (fprec_lt_femax ty) (div_nan ty) BinarySingleNaN.mode_NE x y)
+            (fprec_lt_femax ty) (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x y)
       (Binary.Bmult (fprec ty) (femax ty) (fprec_gt_0 ty) 
-            (fprec_lt_femax ty) (mult_nan ty) BinarySingleNaN.mode_NE x z).
+            (fprec_lt_femax ty) (mult_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x z).
   rewrite E in HMUL.
   rewrite HMUL, HDIV in *; auto.
 Qed.
@@ -458,8 +458,8 @@ Theorem Bdiv_mult_inverse_equiv ty {STD: is_standard ty}:
   Binary.is_finite _ _ z = true ->
   Bexact_inverse (fprec ty) (femax ty) (fprec_gt_0 ty) (fprec_lt_femax ty) y = Some z -> 
   binary_float_equiv
-  (Bdiv _ _ _ (fprec_lt_femax ty) (div_nan ty) BinarySingleNaN.mode_NE x y) 
-  (Bmult _ _ _ (fprec_lt_femax ty) (mult_nan ty) BinarySingleNaN.mode_NE x z) .
+  (Bdiv _ _ _ (fprec_lt_femax ty) (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x y) 
+  (Bmult _ _ _ (fprec_lt_femax ty) (mult_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x z) .
 Proof.
 intros.
 destruct x.
@@ -473,7 +473,7 @@ destruct x.
  + cbv [Bdiv Bmult Binary.build_nan binary_float_equiv]. reflexivity.
 - apply binary_float_eq_equiv.
    apply Bdiv_mult_inverse_finite; auto.
-Qed.
+Qed.  
 
 Theorem Bdiv_mult_inverse_equiv2 ty {STD: is_standard ty}:
   forall x1 x2 y z: (Binary.binary_float (fprec ty) (femax ty)),
@@ -482,8 +482,8 @@ Theorem Bdiv_mult_inverse_equiv2 ty {STD: is_standard ty}:
   Binary.is_finite _ _ z = true ->
   Bexact_inverse (fprec ty) (femax ty) (fprec_gt_0 ty) (fprec_lt_femax ty) y = Some z -> 
   binary_float_equiv
-  (Bdiv _ _ _ (fprec_lt_femax ty) (div_nan ty) BinarySingleNaN.mode_NE x1 y) 
-  (Bmult _ _ _ (fprec_lt_femax ty) (mult_nan ty) BinarySingleNaN.mode_NE x2 z) .
+  (Bdiv _ _ _ (fprec_lt_femax ty) (div_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x1 y) 
+  (Bmult _ _ _ (fprec_lt_femax ty) (mult_nan (fprec ty) (femax ty) (fprec_gt_one ty)) BinarySingleNaN.mode_NE x2 z) .
 Proof.
 intros.
 assert (binary_float_equiv x1 x2) by apply H.
diff --git a/vcfloat/Rounding.v b/vcfloat/Rounding.v
index d6d4989..7b37287 100644
--- a/vcfloat/Rounding.v
+++ b/vcfloat/Rounding.v
@@ -2021,17 +2021,17 @@ Proof.
 
   {
     (* plus *)
-    generalize (Bplus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _) BinarySingleNaN.mode_NE _ _ F1 F2).
+    generalize (Bplus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE _ _ F1 F2).
     change (SpecFloat.fexp _ _) with (FLT_exp (3 - femax ty - fprec ty) (fprec ty)).
     change (BinarySingleNaN.round_mode _) with ZnearestE.
     rewrite <- !FT2R_ftype_of_float, !ftype_of_float_of_ftype.
     rewrite Raux.Rlt_bool_true by lra.
     destruct 1 as (? & ? & _).
     unfold BPLUS, BINOP; rewrite float_of_ftype_of_float; auto.
-  }
+  }  
   {
     (* minus *)
-    generalize (Bminus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _) BinarySingleNaN.mode_NE _ _ F1 F2).
+    generalize (Bminus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE _ _ F1 F2).
     change (SpecFloat.fexp _ _) with (FLT_exp (3 - femax ty - fprec ty) (fprec ty)).
     change (BinarySingleNaN.round_mode _) with ZnearestE.
     rewrite <- !FT2R_ftype_of_float, !ftype_of_float_of_ftype.
@@ -2041,7 +2041,7 @@ Proof.
   }
   {
     (* mult *)
-    generalize (Bmult_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _) BinarySingleNaN.mode_NE (float_of_ftype e1) (float_of_ftype e2)).
+    generalize (Bmult_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE (float_of_ftype e1) (float_of_ftype e2)).
     change (SpecFloat.fexp _ _) with (FLT_exp (3 - femax ty - fprec ty) (fprec ty)).
     change (BinarySingleNaN.round_mode _) with ZnearestE.
     rewrite <- !FT2R_ftype_of_float, !ftype_of_float_of_ftype.
@@ -2052,7 +2052,7 @@ Proof.
     unfold BMULT, BINOP; rewrite float_of_ftype_of_float; auto.
   }
   (* div *)
-  generalize (fun K => Bdiv_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (div_nan _) BinarySingleNaN.mode_NE (float_of_ftype e1) (float_of_ftype e2) K).
+  generalize (fun K => Bdiv_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (div_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE (float_of_ftype e1) (float_of_ftype e2) K).
     change (SpecFloat.fexp _ _) with (FLT_exp (3 - femax ty - fprec ty) (fprec ty)).
     change (BinarySingleNaN.round_mode _) with ZnearestE.
     rewrite <- !FT2R_ftype_of_float, !ftype_of_float_of_ftype.
@@ -2099,7 +2099,7 @@ Proof.
   repeat rewrite B2R_correct in *.
     cbn -[Zminus] in * |- * ;
     rewrite V1 in * |- *.
-    generalize (Bsqrt_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (sqrt_nan _) 
+    generalize (Bsqrt_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (sqrt_nan _ _ (fprec_gt_one _)) 
           BinarySingleNaN.mode_NE (float_of_ftype e1)).
     destruct 1 as (? & ? & _).
     unfold BSQRT, UNOP.
@@ -2326,7 +2326,7 @@ Lemma cast_standard: forall NAN tto tfrom STDto STDfrom f,
     | left r => eq_rect _ _ f _ r
     | _ =>  ftype_of_float
            (Bconv (fprec tfrom) (femax tfrom) (fprec tto) (femax tto)
-                        (fprec_gt_0 _) (fprec_lt_femax _) (conv_nan _ _) 
+                        (fprec_gt_0 _) (fprec_lt_femax _) (conv_nan _ _ _ _ (fprec_gt_one _)) 
                  BinarySingleNaN.mode_NE (float_of_ftype f))
   end.
 Proof.
@@ -2644,7 +2644,7 @@ Proof.
         specialize (H1 _ EB2).
         specialize (H1' _ EB2).
         rewrite is_finite_Binary in F1,F2.
-        generalize (Bminus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _) BinarySingleNaN.mode_NE _ _ F1 F2).
+        generalize (Bminus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE _ _ F1 F2).
         intro K.
         change ( Z.pos (fprecp ty)) with (fprec ty) in K.
         rewrite !B2R_float_of_ftype in *.
@@ -2731,7 +2731,7 @@ Proof.
           destruct minus.
           ++
             unfold BMINUS, BINOP.
-            generalize (Bminus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _) BinarySingleNaN.mode_NE _ _ F1 F2).
+            generalize (Bminus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE _ _ F1 F2).
             rewrite ZERO.
             rewrite Rminus_0_l.
             rewrite Generic_fmt.round_opp.
@@ -2749,7 +2749,7 @@ Proof.
                    is_finite_Binary, float_of_ftype_of_float, BV.
             intuition auto with *.
           ++
-            generalize (Bplus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _) BinarySingleNaN.mode_NE _ _ F1 F2).
+            generalize (Bplus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE _ _ F1 F2).
             rewrite ZERO.
             rewrite Rplus_0_l.
             rewrite Generic_fmt.round_generic
@@ -2771,7 +2771,7 @@ Proof.
           rewrite is_finite_Binary in F1,F2|-*.
           destruct minus.
           {
-          generalize (Bminus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _) BinarySingleNaN.mode_NE _ _ F1 F2).
+          generalize (Bminus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE _ _ F1 F2).
           rewrite ZERO.
           rewrite Rminus_0_r.
           rewrite Generic_fmt.round_generic; try typeclasses eauto.
@@ -2789,7 +2789,7 @@ Proof.
           }
           apply generic_format_B2R.
          }
-         generalize (Bplus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _) BinarySingleNaN.mode_NE _ _ F1 F2).
+         generalize (Bplus_correct _ _  (fprec_gt_0 _) (fprec_lt_femax _) (plus_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE _ _ F1 F2).
          rewrite ZERO.
          rewrite Rplus_0_r.
          rewrite Generic_fmt.round_generic; try typeclasses eauto.
@@ -2945,8 +2945,8 @@ Proof.
     rewrite Z.leb_le in H.
     apply center_Z_correct in H.
     assert (B2_FIN := B2_finite ty (Z.neg pow) (proj2 H)).
-    generalize (Bmult_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) (float_of_ftype (fval env e))).
-    generalize (Bmult_correct_comm _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) (float_of_ftype (fval env e))).
+    generalize (Bmult_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) (float_of_ftype (fval env e))).
+    generalize (Bmult_correct_comm _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE (B2 ty (Z.neg pow)) (float_of_ftype (fval env e))).
     rewrite Rmult_comm.
     change (SpecFloat.fexp (fprec ty) (femax ty))
      with  (FLT_exp (3 - femax ty - fprec ty) (fprec ty)).
@@ -3031,9 +3031,9 @@ Proof.
       generalize (B2_finite ty (Z.of_N pow) (proj2 H)).
       intro B2_FIN.
       generalize
-          (Bmult_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _) BinarySingleNaN.mode_NE (B2 ty (Z.of_N pow)) (float_of_ftype (fval env e))).
+          (Bmult_correct _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE (B2 ty (Z.of_N pow)) (float_of_ftype (fval env e))).
       generalize
-         (Bmult_correct_comm _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _) BinarySingleNaN.mode_NE (B2 ty (Z.of_N pow)) (float_of_ftype (fval env e))).
+         (Bmult_correct_comm _ _ (fprec_gt_0 _) (fprec_lt_femax _) (mult_nan _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE (B2 ty (Z.of_N pow)) (float_of_ftype (fval env e))).
       rewrite Rmult_comm.
       replace (Z.of_N (pow + 1)) with (Z.of_N pow + 1)%Z in H by (rewrite N2Z.inj_add; simpl; ring).
       specialize (H1 _ (or_introl _ (refl_equal _)) _ EB1).
@@ -3119,7 +3119,7 @@ Proof.
     rewrite is_finite_Binary in F1.
     generalize ((fun J1 =>
                   Bconv_widen_exact _ _ _ _ J1 (fprec_gt_0 _) (fprec_lt_femax _) 
-                        (Z.le_ge _ _ H0) (Z.le_ge _ _ H3) (conv_nan _ _) BinarySingleNaN.mode_NE _ F1) ltac:( typeclasses eauto ) ).
+                        (Z.le_ge _ _ H0) (Z.le_ge _ _ H3) (conv_nan _ _ _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE _ F1) ltac:( typeclasses eauto ) ).
     destruct 1 as (K & L & _).
     symmetry in K.
     rewrite B2R_float_of_ftype, <- V1 in K.
@@ -3162,7 +3162,7 @@ Proof.
   destruct K as (errors2 & E & R & EB).
   rewrite V1 in R.
   rewrite is_finite_Binary in F1.
-  generalize (Bconv_correct _ _ _ _ (fprec_gt_0 _) (fprec_lt_femax ty) (conv_nan _ _) BinarySingleNaN.mode_NE _ F1).
+  generalize (Bconv_correct _ _ _ _ (fprec_gt_0 _) (fprec_lt_femax ty) (conv_nan _ _ _ _ (fprec_gt_one _)) BinarySingleNaN.mode_NE _ F1).
   unfold BinarySingleNaN.round_mode.
   rewrite !B2R_float_of_ftype, <- R.
   rewrite Raux.Rlt_bool_true.