diff options
| author | Théo Zimmermann | 2020-06-10 12:29:01 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-10 12:29:01 +0200 |
| commit | 65a64e634ab0f89ba87f826029c8247a48ef82c2 (patch) | |
| tree | 6f7725552c214ca148238fecb87be482d97a58a8 | |
| parent | 95be052f60b1b6b4cc0b12e92b3d1b86b5bd7ca9 (diff) | |
Update changelog for 8.12+beta1.
| -rw-r--r-- | doc/changelog/10-standard-library/12484-fix12483.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 24 |
2 files changed, 18 insertions, 12 deletions
diff --git a/doc/changelog/10-standard-library/12484-fix12483.rst b/doc/changelog/10-standard-library/12484-fix12483.rst deleted file mode 100644 index 95e7c150a3..0000000000 --- a/doc/changelog/10-standard-library/12484-fix12483.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Fix the 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). 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 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |