From 0e83878b0750aaa2b69bb2ff529131ab16d3d64f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 3 Apr 2020 13:58:33 +0200 Subject: Adding changelog for 8.11.1. --- .../01-kernel/11811-uncheck_positivity_bug.rst | 4 -- ...0-master+fix11331-custom-entries-precedence.rst | 8 ---- .../03-notations/11859-warn-inexact-float.rst | 6 --- .../09-coqide/10008-snyke7+escape_spaces.rst | 4 -- .../11131-ci+back_to_ocaml_410.rst | 7 --- .../11860-ci+ocaml_to_4091.rst | 4 -- ...fix11114-extraction-anomaly-implicit-record.rst | 4 -- doc/sphinx/changes.rst | 51 ++++++++++++++++++++++ 8 files changed, 51 insertions(+), 37 deletions(-) delete mode 100644 doc/changelog/01-kernel/11811-uncheck_positivity_bug.rst delete mode 100644 doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst delete mode 100644 doc/changelog/03-notations/11859-warn-inexact-float.rst delete mode 100644 doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/11131-ci+back_to_ocaml_410.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/11860-ci+ocaml_to_4091.rst delete mode 100644 doc/changelog/12-misc/11329-master+fix11114-extraction-anomaly-implicit-record.rst 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 `_, - 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 `_, - by Hugo Herbelin, fixing in particular - `#9517 `_, - `#9519 `_, - `#9521 `_, - `#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 `_, - 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 `_, - by snyke7, fixing `#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 `_, - `#11123 `_, - `#11102 `_, - 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 `_, - 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 `_, - by Hugo Herbelin, fixes `#11114 `_). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 7401aff48c..31fb1b7382 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -647,6 +647,57 @@ Changes in 8.11.0 (`#11227 `_, by Bernhard M. Wiedemann). +Changes in 8.11.1 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Fixed:** + Allow more inductive types in `Unset Positivity Checking` mode + (`#11811 `_, + by SimonBoulier). + +**Notations** + +- **Fixed:** + Bugs in dealing with precedences of notations in custom entries + (`#11530 `_, + by Hugo Herbelin, fixing in particular + `#9517 `_, + `#9519 `_, + `#9521 `_, + `#11331 `_). +- **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 `_, + by Pierre Roux). + +**CoqIDE** + +- **Fixed:** + Compiling file paths containing spaces + (`#10008 `_, + by snyke7, fixing `#11595 `_). + +**Infrastructure and dependencies** + +- **Added:** + Bump official OCaml support and CI testing to 4.10.0 + (`#11131 `_, + `#11123 `_, + `#11102 `_, + by Emilio Jesus Gallego Arias, Jacques-Henri Jourdan, + Guillaume Melquiond, and Guillaume Munch-Maccagnoni). + +**Miscellaneous** + +- **Fixed:** + :cmd:`Extraction Implicit` on the constructor of a record was leading to an anomaly + (`#11329 `_, + by Hugo Herbelin, fixes `#11114 `_). + Version 8.10 ------------ -- cgit v1.2.3