Merge PR #11986: [primitive floats] Add low level printing

Ack-by: SkySkimmer
Reviewed-by: ppedrot

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