diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8097935ec2..63079993c8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -888,12 +888,19 @@ let q_infinity () = qualid_of_ref "num.float.infinity" let q_neg_infinity () = qualid_of_ref "num.float.neg_infinity" let q_nan () = qualid_of_ref "num.float.nan" +let get_printing_float = Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Float"] + ~value:true + let extern_float f scopes = if Float64.is_nan f then CRef(q_nan (), None) else if Float64.is_infinity f then CRef(q_infinity (), None) else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None) else - let s = Float64.(to_string f) in + let s = + let hex = !Flags.raw_print || not (get_printing_float ()) in + if hex then Float64.to_hex_string f else Float64.to_string f in let n = NumTok.Signed.of_string s in extern_prim_token_delimiter_if_required (Numeral n) "float" "float_scope" scopes |