Add Proof keyword so that documentation generation works

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2520 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 2 insertions, 0 deletions

diff --git a/lib/Floats.v b/lib/Floats.v
index 10d2dc5..35009d8 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -124,6 +124,7 @@ Global Opaque binary_normalize32_correct.
 (* The Nan payload operations for single <-> double conversions are not part of
    the IEEE754 standard, but shared between all architectures of Compcert. *)
 Definition floatofbinary32_pl (s:bool) (pl:nan_pl 24) : (bool * nan_pl 53).
+Proof.
   refine (s, transform_quiet_pl (exist _ (Pos.shiftl_nat (proj1_sig pl) 29) _)).
   abstract (
     destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_iter, Fcore_digits.digits2_Pnat;
@@ -133,6 +134,7 @@ Definition floatofbinary32_pl (s:bool) (pl:nan_pl 24) : (bool * nan_pl 53).
 Defined.
 
 Definition binary32offloat_pl (s:bool) (pl:nan_pl 53) : (bool * nan_pl 24).
+Proof.
   refine (s, exist _ (Pos.shiftr_nat (proj1_sig (transform_quiet_pl pl)) 29) _).
   abstract (
     destruct (transform_quiet_pl pl); unfold proj1_sig, Pos.shiftr_nat, nat_iter;