diff options
| author | Théo Zimmermann | 2020-04-03 14:43:37 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-03 14:43:37 +0200 |
| commit | acefe58cd39c9a4efee632f7f92f56fb4d5285bb (patch) | |
| tree | 1a960a9f1c970d54865cd94c21ec1a743afdfdfc /doc/changelog | |
| parent | e46e37ddabcb5ef2d58fd09dcc0a13a4b42f6b93 (diff) | |
| parent | 0e83878b0750aaa2b69bb2ff529131ab16d3d64f (diff) | |
Merge PR #12009: Adding changelog for 8.11.1.
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/changelog')
7 files changed, 0 insertions, 37 deletions
diff --git a/doc/changelog/01-kernel/11811-uncheck_positivity_bug.rst b/doc/changelog/01-kernel/11811-uncheck_positivity_bug.rst deleted file mode 100644 index c08ebb7f25..0000000000 --- a/doc/changelog/01-kernel/11811-uncheck_positivity_bug.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Allow more inductive types in `Unset Positivity Checking` mode - (`#11811 <https://github.com/coq/coq/pull/11811>`_, - by SimonBoulier). diff --git a/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst deleted file mode 100644 index b105928b22..0000000000 --- a/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - Bugs in dealing with precedences of notations in custom entries - (`#11530 <https://github.com/coq/coq/pull/11530>`_, - by Hugo Herbelin, fixing in particular - `#9517 <https://github.com/coq/coq/pull/9517>`_, - `#9519 <https://github.com/coq/coq/pull/9519>`_, - `#9521 <https://github.com/coq/coq/pull/9521>`_, - `#11331 <https://github.com/coq/coq/pull/11331>`_). diff --git a/doc/changelog/03-notations/11859-warn-inexact-float.rst b/doc/changelog/03-notations/11859-warn-inexact-float.rst deleted file mode 100644 index 224ffdbe9b..0000000000 --- a/doc/changelog/03-notations/11859-warn-inexact-float.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - In primitive floats, print a warning when parsing a decimal value - that is not exactly a binary64 floating-point number. - For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't. - (`#11859 <https://github.com/coq/coq/pull/11859>`_, - by Pierre Roux). diff --git a/doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst b/doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst deleted file mode 100644 index cbd97688c3..0000000000 --- a/doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Compiling file paths containing spaces - (`#10008 <https://github.com/coq/coq/pull/10008>`_, - by snyke7, fixing `#11595 <https://github.com/coq/coq/pull/11595>`_). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11131-ci+back_to_ocaml_410.rst b/doc/changelog/11-infrastructure-and-dependencies/11131-ci+back_to_ocaml_410.rst deleted file mode 100644 index 778d37e07b..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/11131-ci+back_to_ocaml_410.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - Bump official OCaml support and CI testing to 4.10.0 - (`#11131 <https://github.com/coq/coq/pull/11131>`_, - `#11123 <https://github.com/coq/coq/pull/11123>`_, - `#11102 <https://github.com/coq/coq/pull/11123>`_, - by Emilio Jesus Gallego Arias, Jacques-Henri Jourdan, - Guillaume Melquiond, and Guillaume Munch-Maccagnoni). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11860-ci+ocaml_to_4091.rst b/doc/changelog/11-infrastructure-and-dependencies/11860-ci+ocaml_to_4091.rst deleted file mode 100644 index 94e2c34828..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/11860-ci+ocaml_to_4091.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Bump official OCaml support to 4.09.1 - (`#11860 <https://github.com/coq/coq/pull/11860>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/12-misc/11329-master+fix11114-extraction-anomaly-implicit-record.rst b/doc/changelog/12-misc/11329-master+fix11114-extraction-anomaly-implicit-record.rst deleted file mode 100644 index 0a686dd87d..0000000000 --- a/doc/changelog/12-misc/11329-master+fix11114-extraction-anomaly-implicit-record.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - :cmd:`Extraction Implicit` on the constructor of a record was leading to an anomaly - (`#11329 <https://github.com/coq/coq/pull/11329>`_, - by Hugo Herbelin, fixes `#11114 <https://github.com/coq/coq/pull/11114>`_). |
