diff options
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 b6f48ae..e6f1e2c 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"; |