diff options
| author | Erik Martin-Dorel | 2019-06-27 20:43:15 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:21:25 +0100 |
| commit | 3352f539d271b4161556238da071861b4700da93 (patch) | |
| tree | 641607900749f33ee5656cd1f0b6ce25f8370c8a | |
| parent | d5f49c85630e25f2c2b45cf03cc3f589e7cdaf5f (diff) | |
docs: Add entry in changelog
| -rw-r--r-- | doc/changelog/01-kernel/09867-floats.rst | 13 |
1 files changed, 13 insertions, 0 deletions
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 <https://github.com/coq/coq/pull/9867>`_, + closes `#8276 <https://github.com/coq/coq/issues/8276>`_, + by Guillaume Bertholon, Erik Martin-Dorel, Pierre Roux). |