diff --git a/src_common/ieee/coq/.gitignore b/src_common/ieee/coq/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..cc786a9724d1c928c856bdcbef4ce2acdc6ede2d
--- /dev/null
+++ b/src_common/ieee/coq/.gitignore
@@ -0,0 +1 @@
+doc/
\ No newline at end of file
diff --git a/src_common/ieee/coq/B32.v b/src_common/ieee/coq/B32.v
index 3575fe4bcd9185540dce3c6eb06069fc9ca2334e..dcc3ac127c455744d604750abb3d5cd38d38e4e5 100644
--- a/src_common/ieee/coq/B32.v
+++ b/src_common/ieee/coq/B32.v
@@ -9,25 +9,39 @@ Require Import Extraction.
 From F Require Import Qextended Rextended.
 
 
+(** * An instanciation of Flocq's BinarySingleNan for 32 bits IEEE-754 floating points *)
+
 Module B32.
 
+(** ** 1. Precision, maximal exponent & their properties *)
+
 Definition prec : Z := 24.
 Definition emax : Z := 128.
-
 Definition mw : Z := 23.
 Definition ew : Z := 8.
-
 Definition t : Type := binary_float prec emax.
 
 Lemma Hprec : Prec_gt_0 prec.
-  Proof. unfold Prec_gt_0, prec; lia. Qed.
+Proof.
+  unfold Prec_gt_0, prec; lia.
+Qed.
 
 Lemma Hemax : Prec_lt_emax prec emax.
-  Proof. unfold Prec_lt_emax, prec, emax; lia. Qed.
+Proof.
+  unfold Prec_lt_emax, prec, emax; lia.
+Qed.
 
-Lemma Hmw : (0 < mw)%Z. unfold mw; lia. Qed.
+Lemma Hmw : (0 < mw)%Z.
+Proof.
+  unfold mw; lia.
+Qed.
 
-Lemma Hew : (0 < ew)%Z. unfold ew; lia. Qed.
+Lemma Hew : (0 < ew)%Z.
+Proof.
+  unfold ew; lia.
+Qed.
+
+(** ** 2. Floating-points operators *)
 
 Definition add : mode -> t -> t -> t := @Bplus _ _ Hprec Hemax.
 Definition sub : mode -> t -> t -> t := @Bminus _ _ Hprec Hemax.
@@ -36,12 +50,16 @@ Definition div : mode -> t -> t -> t := @Bmult _ _ Hprec Hemax.
 Definition sqrt : mode -> t -> t := @Bsqrt _ _ Hprec Hemax.
 Definition abs : t -> t := Babs.
 
+(** ** 3. Floating-points relations *)
+
 Definition le : t -> t -> bool := Bleb.
 Definition lt : t -> t -> bool := Bltb.
 Definition eq : t -> t -> bool := Beqb.
 Definition ge : t -> t -> bool := fun x y => Bleb y x.
 Definition gt : t -> t -> bool := fun x y => Bltb y x.
 
+(** ** 4. convertions to and from [Z] and [Q]*)
+
 Definition of_bits (b : Z) : t :=
   match Bits.binary_float_of_bits mw ew Hmw Hew Hemax b with
   | Binary.B754_nan _ _ _ _ _ => B754_nan
diff --git a/src_common/ieee/coq/Intv32.v b/src_common/ieee/coq/Intv32.v
index 88c517246b551de97b8928f066e14f1a5fe718b4..7dc0ea446a412799e17261f36e5ae2a03fed0940 100644
--- a/src_common/ieee/coq/Intv32.v
+++ b/src_common/ieee/coq/Intv32.v
@@ -110,19 +110,6 @@ Module Intv32.
       contains_opt (fst (eq_inv I1 I2)) x /\ contains_opt (snd (eq_inv I1 I2)) y.
   Proof. apply (@Ieq_inv_correct prec emax). Qed.
 
-
-
-
-
-
-
-  
-    
-  Qed.
-  
-
-
-
 End Intv32.
 
 Require Import Sumbool.
diff --git a/src_common/ieee/coq/Makefile b/src_common/ieee/coq/Makefile
index 5d5d859342cfb12495077c082965edf1c6f21695..ab47ada5401e4fab3302e9bbf6f8acfa41dce229 100644
--- a/src_common/ieee/coq/Makefile
+++ b/src_common/ieee/coq/Makefile
@@ -1,4 +1,13 @@
 include CoqMakefile
 
 CoqMakefile:
-	coq_makefile -f _CoqProject -o CoqMakefile
\ No newline at end of file
+	@ coq_makefile -f _CoqProject -o CoqMakefile
+
+.PHONY: cleandoc doc
+
+cleandoc:
+	@ rm -rf doc/
+
+doc:
+	@ mkdir -p doc
+	@ coq2html -base F *.v *.glob -d doc -redirect
\ No newline at end of file
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index 5262270bc8087761209e55d18a2bbc9e07197026..7444891bdfef9375f531dc9a9e73ede905ffcfa3 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -153,13 +153,10 @@ Definition round (m : mode) (r : Rx) : Rx :=
   | _  => r
   end.
 
-
-
 Lemma dont_overflow_inv :
   forall m (r : R),
     do_overflow m r = false ->
     exists (f : float), Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) r = B2R f /\ is_finite f = true.
-    (* exists mr er Hb, Generic_fmt.round Zaux.radix2 fexp (round_mode m) r = @B2R prec emax (B754_finite (sign r) mr er Hb). *)
 Proof.
   intros mode r H.
   apply do_overflow_false in H.