diff options
Diffstat (limited to 'exportclight/ExportClight.ml')
-rw-r--r-- | exportclight/ExportClight.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 409abcfa..02f1249c 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 |