summaryrefslogtreecommitdiff
path: root/exportclight
diff options
context:
space:
mode:
Diffstat (limited to 'exportclight')
-rw-r--r--exportclight/ExportClight.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 409abcf..02f1249 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -121,10 +121,10 @@ let coqint p n =
else fprintf p "(Int.repr (%ld))" n
let coqfloat p n =
- let n = camlint64_of_coqint(Floats.Float.bits_of_double n) in
+ let n = camlint64_of_coqint(Floats.Float.to_bits n) in
if n >= 0L
- then fprintf p "(Float.double_of_bits (Int64.repr %Ld))" n
- else fprintf p "(Float.double_of_bits (Int64.repr (%Ld)))" n
+ then fprintf p "(Float.of_bits (Int64.repr %Ld))" n
+ else fprintf p "(Float.of_bits (Int64.repr (%Ld)))" n
let coqint64 p n =
let n = camlint64_of_coqint n in