diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 08:18:51 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 08:18:51 +0000 |
commit | d71a5cfd10378301b71d32659d5936e01d72ae50 (patch) | |
tree | 9b6a7cc437ab205b7e0bf5bf90585451d8a8c367 /lib/Integers.v | |
parent | 913c1bcc4b2204afd447edd723e06b905fd1f47f (diff) | |
download | compcert-kvx-d71a5cfd10378301b71d32659d5936e01d72ae50.tar.gz compcert-kvx-d71a5cfd10378301b71d32659d5936e01d72ae50.zip |
Revised encoding/decoding of floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Integers.v')
-rw-r--r-- | lib/Integers.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index d047199d..f2aca962 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -2770,7 +2770,7 @@ Qed. End Make. -(** * Specialization to 32-bit integers and to bytes. *) +(** * Specialization to integers of size 8, 32, and 64 bits *) Module Wordsize_32. Definition wordsize := 32%nat. @@ -2797,3 +2797,15 @@ End Wordsize_8. Module Byte := Integers.Make(Wordsize_8). Notation byte := Byte.int. + +Module Wordsize_64. + Definition wordsize := 64%nat. + Remark wordsize_not_zero: wordsize <> 0%nat. + Proof. unfold wordsize; congruence. Qed. +End Wordsize_64. + +Module Int64 := Make(Wordsize_64). + +Notation int64 := Int64.int. + + |