From 09e5a3fc4a0f03593a654ecb4285622f7e5abfb9 Mon Sep 17 00:00:00 2001 From: jjourdan Date: Fri, 4 Jul 2014 12:01:59 +0000 Subject: 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 --- lib/Floats.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib') 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; -- cgit v1.2.3