Merge PR coq#18035: Document the roughness of the Floats library

Reviewed-by: silene Reviewed-by: JasonGross Ack-by: jfehrle Co-authored-by: silene <[email protected]>
SkySkimmer · Sep 18, 2023 · b881f18 · b881f18
2 parents a99e6ec + 31c3d8b
commit b881f18
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 1 deletion.
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
@@ -989,6 +989,15 @@ Notation    Interpretation  Precedence  Associativity
 Floats library
 ~~~~~~~~~~~~~~
 
+The standard library has a small ``Floats`` module for accessing
+processor floating-point operations through the Coq kernel.
+However, while this module supports computation and has a bit-level
+specification, it doesn't include elaborate theorems, such as a link
+to real arithmetic or various error bounds. To do proofs by
+reflection, use ``Floats`` in conjunction with the complementary
+`Flocq <https://flocq.gitlabpages.inria.fr/>`_ library, which provides
+many such theorems.
+
 The library of primitive floating-point arithmetic can be loaded by
 requiring module ``Floats``:
 

diff --git a/theories/Floats/Floats.v b/theories/Floats/Floats.v
@@ -17,7 +17,11 @@
 - FloatLemmas: prove a few results involving Z.frexp and Z.ldexp
 
 For a brief overview of the Floats library,
-see {{https://coq.inria.fr/distrib/current/refman/language/coq-library.html#floats-library}} *)
+see {{https://coq.inria.fr/distrib/current/refman/language/coq-library.html#floats-library}}
+
+N.B.: This library only offers a bit-level specification of floating-point
+arithmetic. For a more complete set of theorems, including links with real
+arithmetic, see the Flocq library {{https://flocq.gitlabpages.inria.fr/}} *)
 
 Require Export FloatClass.
 Require Export PrimFloat.