diff --git a/src/Appli/Fappli_IEEE.v b/src/Appli/Fappli_IEEE.v
index e5b038bb4096694897ceba3aea31e5db81165ada..bb747e3a28f2443b317c3d2d0b5130cd9b15a11b 100644
--- a/src/Appli/Fappli_IEEE.v
+++ b/src/Appli/Fappli_IEEE.v
@@ -199,7 +199,7 @@ Qed.
 Theorem FLT_format_B2R :
   forall x,
   FLT_format radix2 emin prec (B2R x).
-Proof.
+Proof with auto with typeclass_instances.
 intros x.
 apply FLT_format_generic...
 apply generic_format_B2R.