From ec99f20895f8b12faba3dd868b88a4eae1aec967 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 6 Sep 2012 22:26:42 +0200
Subject: [PATCH] Prove FLT_format_B2R.

---
 src/Appli/Fappli_IEEE.v | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/Appli/Fappli_IEEE.v b/src/Appli/Fappli_IEEE.v
index 63b150f..e5b038b 100644
--- a/src/Appli/Fappli_IEEE.v
+++ b/src/Appli/Fappli_IEEE.v
@@ -196,6 +196,15 @@ apply canonic_canonic_mantissa.
 now destruct (andb_prop _ _ Hx) as (H, _).
 Qed.
 
+Theorem FLT_format_B2R :
+  forall x,
+  FLT_format radix2 emin prec (B2R x).
+Proof.
+intros x.
+apply FLT_format_generic...
+apply generic_format_B2R.
+Qed.
+
 Theorem B2FF_inj :
   forall x y : binary_float,
   B2FF x = B2FF y ->
@@ -317,15 +326,12 @@ rewrite <- F2R_opp.
 now case sx.
 Qed.
 
-
 Theorem is_finite_Bopp: forall x,
   is_finite (Bopp x) = is_finite x.
 Proof.
 now intros [| | |].
 Qed.
 
-
-
 Theorem bounded_lt_emax :
   forall mx ex,
   bounded mx ex = true ->
-- 
GitLab