diff options
Diffstat (limited to 'aarch64/TargetPrinter.ml')
-rw-r--r-- | aarch64/TargetPrinter.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 5b3919d3..b5e3a814 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -416,7 +416,7 @@ module Target (*: TARGET*) = fprintf oc " fmov %a, %a\n" dreg rd dreg r1 | Pfmovimmd(rd, f) -> let d = camlint64_of_coqint (Floats.Float.to_bits f) in - if Asmblock.is_immediate_float64 f then + if is_immediate_float64 f then fprintf oc " fmov %a, #%.7f\n" dreg rd (Int64.float_of_bits d) else begin let lbl = label_literal64 d in @@ -425,7 +425,7 @@ module Target (*: TARGET*) = end | Pfmovimms(rd, f) -> let d = camlint_of_coqint (Floats.Float32.to_bits f) in - if Asmblock.is_immediate_float32 f then + if is_immediate_float32 f then fprintf oc " fmov %a, #%.7f\n" sreg rd (Int32.float_of_bits d) else begin let lbl = label_literal32 d in |