Print a warning when parsing non floating-point values.

For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.

2 files changed, 11 insertions, 0 deletions

diff --git a/doc/changelog/03-notations/11859-warn-inexact-float.rst b/doc/changelog/03-notations/11859-warn-inexact-float.rst
new file mode 100644
index 0000000000..224ffdbe9b
--- /dev/null
+++ b/doc/changelog/03-notations/11859-warn-inexact-float.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  In primitive floats, print a warning when parsing a decimal value
+  that is not exactly a binary64 floating-point number.
+  For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
+  (`#11859 <https://github.com/coq/coq/pull/11859>`_,
+  by Pierre Roux).
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 39f2ccec29..acdd4408ed 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -1062,6 +1062,11 @@ Floating-point constants are parsed and pretty-printed as (17-digit)
 decimal constants. This ensures that the composition
 :math:`\text{parse} \circ \text{print}` amounts to the identity.
 
+.. warn:: The constant @numeral is not a binary64 floating-point value.  A closest value will be used and unambiguously printed @numeral. [inexact-float,parsing]
+
+   Not all decimal constants are floating-point values. This warning
+   is generated when parsing such a constant (for instance ``0.1``).
+
 .. example::
 
   .. coqtop:: all