From 6f3718869f6ac76dfac4f2223206e6d75c0c00c9 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 24 Sep 2012 18:19:35 +0700
Subject: [PATCH] Fix compilation with Coq 8.4.

---
 src/Appli/Fappli_IEEE.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Appli/Fappli_IEEE.v b/src/Appli/Fappli_IEEE.v
index e5b038b..bb747e3 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.
-- 
GitLab