diff options
Diffstat (limited to 'doc/changelog/01-kernel/09867-floats.rst')
| -rw-r--r-- | doc/changelog/01-kernel/09867-floats.rst | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/doc/changelog/01-kernel/09867-floats.rst b/doc/changelog/01-kernel/09867-floats.rst deleted file mode 100644 index cae4dbb335..0000000000 --- a/doc/changelog/01-kernel/09867-floats.rst +++ /dev/null @@ -1,14 +0,0 @@ -- **Added:** - A built-in support of floating-point arithmetic, allowing - one to devise efficient reflection tactics involving numerical - computation. Primitive floats are added in the language of terms, - following the binary64 format of the IEEE 754 standard, and the - related operations are implemented for the different reduction - engines of Coq by using the corresponding processor operators in - rounding-to-nearest-even. The properties of these operators are - axiomatized in the theory :g:`Coq.Floats.FloatAxioms` which is part - of the library :g:`Coq.Floats.Floats`. - See Section :ref:`primitive-floats` - (`#9867 <https://github.com/coq/coq/pull/9867>`_, - closes `#8276 <https://github.com/coq/coq/issues/8276>`_, - by Guillaume Bertholon, Erik Martin-Dorel, Pierre Roux). |