diff options
author | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-03 09:15:24 +0000 |
---|---|---|
committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-03 09:15:24 +0000 |
commit | c677d5021a9a6e057b15cf9df8ca9ce7c0f5ae30 (patch) | |
tree | 765798824239f826f5cd008eecf1fdb0ea6820f6 /checklink/Library.ml | |
parent | 3de3ecc23d8ab5d6d45451075467dd70981f1061 (diff) | |
download | compcert-c677d5021a9a6e057b15cf9df8ca9ce7c0f5ae30.tar.gz compcert-c677d5021a9a6e057b15cf9df8ca9ce7c0f5ae30.zip |
checklink: adaptation to the new floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1949 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/Library.ml')
-rw-r--r-- | checklink/Library.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/checklink/Library.ml b/checklink/Library.ml index b6f48aef..e6f1e2cb 100644 --- a/checklink/Library.ml +++ b/checklink/Library.ml @@ -1,5 +1,6 @@ open BinInt open BinPos +open Camlcoq type bitstring = Bitstring.bitstring @@ -112,6 +113,8 @@ let z_int_lax z = Safe32.to_int (z_int32_lax z) (* Some more printers *) +let string_of_ffloat f = string_of_float (camlfloat_of_coqfloat f) + let string_of_array string_of_elt sep a = let b = Buffer.create 1024 in Buffer.add_string b "[\n"; |