From 3352f539d271b4161556238da071861b4700da93 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 27 Jun 2019 20:43:15 +0200 Subject: docs: Add entry in changelog --- doc/changelog/01-kernel/09867-floats.rst | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 doc/changelog/01-kernel/09867-floats.rst (limited to 'doc') diff --git a/doc/changelog/01-kernel/09867-floats.rst b/doc/changelog/01-kernel/09867-floats.rst new file mode 100644 index 0000000000..56b5fc747a --- /dev/null +++ b/doc/changelog/01-kernel/09867-floats.rst @@ -0,0 +1,13 @@ +- A built-in support of floating-point arithmetic was added, 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 `_, + closes `#8276 `_, + by Guillaume Bertholon, Erik Martin-Dorel, Pierre Roux). -- cgit v1.2.3