aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/changes.rst
diff options
context:
space:
mode:
authorThéo Zimmermann2020-06-10 12:29:01 +0200
committerThéo Zimmermann2020-06-10 12:29:01 +0200
commit65a64e634ab0f89ba87f826029c8247a48ef82c2 (patch)
tree6f7725552c214ca148238fecb87be482d97a58a8 /doc/sphinx/changes.rst
parent95be052f60b1b6b4cc0b12e92b3d1b86b5bd7ca9 (diff)
Update changelog for 8.12+beta1.
Diffstat (limited to 'doc/sphinx/changes.rst')
-rw-r--r--doc/sphinx/changes.rst24
1 files changed, 18 insertions, 6 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 51c80e697e..8427300dc4 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -96,6 +96,16 @@ Changes in 8.12+beta1
.. contents::
:local:
+Kernel
+^^^^^^
+
+- **Fixed:**
+ Specification of :n:`PrimFloat.leb` which made
+ :n:`(x <= y)%float` true for any non NaN :n:`x` and :n:`y`.
+ (`#12484 <https://github.com/coq/coq/pull/12484>`_,
+ fixes `#12483 <https://github.com/coq/coq/issues/12483>`_,
+ by Pierre Roux).
+
Specification language, type inference
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -1040,8 +1050,9 @@ Reference manual
`#11423 <https://github.com/coq/coq/pull/11423>`_,
`#11705 <https://github.com/coq/coq/pull/11705>`_,
`#11718 <https://github.com/coq/coq/pull/11718>`_,
- `#11720 <https://github.com/coq/coq/pull/11720>`_
- and `#11961 <https://github.com/coq/coq/pull/11961>`_, by Jim
+ `#11720 <https://github.com/coq/coq/pull/11720>`_,
+ `#11961 <https://github.com/coq/coq/pull/11961>`_
+ and `#12103 <https://github.com/coq/coq/pull/12103>`_, by Jim
Fehrle, reviewed by Théo Zimmermann).
- **Added:**
A glossary of terms and an index of attributes
@@ -1068,10 +1079,11 @@ Reference manual
`#11720 <https://github.com/coq/coq/pull/11720>`_
`#11797 <https://github.com/coq/coq/pull/11797>`_,
`#11913 <https://github.com/coq/coq/pull/11913>`_,
- `#11958 <https://github.com/coq/coq/pull/11958>`_
- `#11960 <https://github.com/coq/coq/pull/11960>`_
- and `#11961 <https://github.com/coq/coq/pull/11961>`_, by Jim
- Fehrle, reviewed by Théo Zimmermann).
+ `#11958 <https://github.com/coq/coq/pull/11958>`_,
+ `#11960 <https://github.com/coq/coq/pull/11960>`_,
+ `#11961 <https://github.com/coq/coq/pull/11961>`_
+ and `#12103 <https://github.com/coq/coq/pull/12103>`_, by Jim
+ Fehrle, reviewed by Théo Zimmermann and Jason Gross).
Infrastructure and dependencies
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^