From c677d5021a9a6e057b15cf9df8ca9ce7c0f5ae30 Mon Sep 17 00:00:00 2001
From: varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 3 Jul 2012 09:15:24 +0000
Subject: checklink: adaptation to the new floats

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1949 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 checklink/Library.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'checklink/Library.ml')

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";
-- 
cgit v1.2.3