diff options
author | jjourdan <jjourdan@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-04 12:01:59 +0000 |
---|---|---|
committer | jjourdan <jjourdan@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-04 12:01:59 +0000 |
commit | 09e5a3fc4a0f03593a654ecb4285622f7e5abfb9 (patch) | |
tree | ce39bbce280998e022676bf1141db6342086ede3 | |
parent | 39528cfffaa5fd3a7e8d20874364141c694b99a7 (diff) | |
download | compcert-09e5a3fc4a0f03593a654ecb4285622f7e5abfb9.tar.gz compcert-09e5a3fc4a0f03593a654ecb4285622f7e5abfb9.zip |
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
-rw-r--r-- | lib/Floats.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index 10d2dc5b..35009d82 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; |