diff --git a/src_common/ieee/coq/finterval.v b/src_common/ieee/coq/Finterval.v
similarity index 98%
rename from src_common/ieee/coq/finterval.v
rename to src_common/ieee/coq/Finterval.v
index 8d3e27755900548782c7ba3e4526224a003f5b47..87e5aa381126c3fc6cafc62de1b7293b2a666522 100644
--- a/src_common/ieee/coq/finterval.v
+++ b/src_common/ieee/coq/Finterval.v
@@ -1,6 +1,10 @@
 From Flocq Require Import IEEE754.BinarySingleNaN.
 From Coq Require Import QArith Psatz Reals Extraction.
 
+(*********************************************************
+       Interval arithmetic over floatting points
+**********************************************************)
+
 Definition emax := 128%Z.
 Definition prec := 24%Z.
 
diff --git a/src_common/ieee/coq/Futils.v b/src_common/ieee/coq/Futils.v
index fcca5e6e33160b0bb57d5ae20b2697f1b1f871b9..b6347500c07b77e0c7ee92fbe0695b89c24b9d87 100644
--- a/src_common/ieee/coq/Futils.v
+++ b/src_common/ieee/coq/Futils.v
@@ -1,6 +1,8 @@
 From Flocq Require Import IEEE754.BinarySingleNaN.
 From Coq Require Import ZArith Lia Reals Psatz.
 
+Section B32.
+
 Definition emax := 128%Z.
 Definition prec := 24%Z.
 
@@ -17,10 +19,7 @@ Lemma prec_gt_0 :
     FLX.Prec_gt_0 prec.
 Proof. def_op. Qed.
 
-Program Definition Fadd (m : mode) := @Bplus prec emax _ _ m.
-Solve All Obligations with def_op.
-
-Compute (Fadd mode_NE B754_nan B754_nan).
+End B32.
 
 Program Definition Flt := @Bltb prec emax.
 
@@ -68,7 +67,7 @@ Proof.
   pose proof (Hc1 := Bplus_correct prec emax H1 H2 m w y Fw Fy).
   pose proof (Hc2 := Bplus_correct prec emax H1 H2 m x z Fx Fz).
   rewrite Ho1 in Hc1. rewrite Ho2 in Hc2.
-  unfold Fadd; simpl; intuition.
+  simpl; intuition.
   rewrite H, H3.
   apply Generic_fmt.round_le; try red; intuition; try ulia; lra.
 Qed.