Pretty-printing primitive float constants

* map special floats to registered CRef's
* kernel/float64.mli: add {is_infinity, is_neg_infinity} functions
* kernel/float64.ml: Replace string_of_float with a safe pretty-printing function

Namely:

  let to_string_raw f = Printf.sprintf "%.17g" f
  let to_string f = if is_nan f then "nan" else to_string_raw f

Summary:

* printing a binary64 float in 17 decimal places and parsing it again
  will yield the same float, e.g.:

  let f1 = 1. +. (0x1p-53 +. 0x1p-105)
  let f2 = float_of_string (to_string f1)
  f1 = f2

* OCaml's string_of_float gives a sign to nan values which shouldn't be
  displayed as all NaNs are considered equal here.

2 files changed, 74 insertions, 0 deletions

diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
new file mode 100644
index 0000000000..f67119020e
--- /dev/null
+++ b/test-suite/output/FloatSyntax.out
@@ -0,0 +1,40 @@
+2%float
+     : float
+2.5%float
+     : float
+(-2.5)%float
+     : float
+2.5e+20%float
+     : float
+(-2.4999999999999999e-20)%float
+     : float
+(2 + 2)%float
+     : float
+(2.5 + 2.5)%float
+     : float
+2
+     : float
+2.5
+     : float
+-2.5
+     : float
+2.5e+20
+     : float
+-2.4999999999999999e-20
+     : float
+2 + 2
+     : float
+2.5 + 2.5
+     : float
+2
+     : nat
+2%float
+     : float
+t = 2%flt
+     : float
+t = 2%flt
+     : float
+2
+     : nat
+2
+     : float
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
new file mode 100644
index 0000000000..1caa0bb444
--- /dev/null
+++ b/test-suite/output/FloatSyntax.v
@@ -0,0 +1,34 @@
+Require Import Floats.
+
+Check 2%float.
+Check 2.5%float.
+Check (-2.5)%float.
+Check 2.5e20%float.
+Check (-2.5e-20)%float.
+Check (2 + 2)%float.
+Check (2.5 + 2.5)%float.
+
+Open Scope float_scope.
+
+Check 2.
+Check 2.5.
+Check (-2.5).
+Check 2.5e20.
+Check (-2.5e-20).
+Check (2 + 2).
+Check (2.5 + 2.5).
+
+Open Scope nat_scope.
+
+Check 2.
+Check 2%float.
+
+Delimit Scope float_scope with flt.
+Definition t := 2%float.
+Print t.
+Delimit Scope nat_scope with float.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
+Close Scope float_scope.