diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-09-24 14:39:49 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-09-24 14:39:49 +0200 |
| commit | 6087efa0b68ae3a1b003dac86970719728976395 (patch) | |
| tree | 86ab889c31888263dbf9e3177fa90a62c0896fad /exportclight/ExportClight.ml | |
| parent | 795485179071254bfab493dd6733d45b8f272900 (diff) | |
| download | compcert-kvx-6087efa0b68ae3a1b003dac86970719728976395.tar.gz compcert-kvx-6087efa0b68ae3a1b003dac86970719728976395.zip | |
Refactoring in the printing of FP numbers.
Diffstat (limited to 'exportclight/ExportClight.ml')
| -rw-r--r-- | exportclight/ExportClight.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index fe2cfded..e4d1ce53 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -127,16 +127,10 @@ let coqint64 p n = else fprintf p "(Int64.repr (%Ld))" n let coqfloat p n = - let n = camlint64_of_coqint(Floats.Float.to_bits n) in - if n >= 0L - then fprintf p "(Float.of_bits (Int64.repr %Ld))" n - else fprintf p "(Float.of_bits (Int64.repr (%Ld)))" n + fprintf p "(Float.of_bits %a)" coqint64 (Floats.Float.to_bits n) let coqsingle p n = - let n = camlint_of_coqint(Floats.Float32.to_bits n) in - if n >= 0l - then fprintf p "(Float32.of_bits (Int.repr %ld))" n - else fprintf p "(Float32.of_bits (Int.repr (%ld)))" n + fprintf p "(Float32.of_bits %a)" coqint (Floats.Float32.to_bits n) (* Types *) |