From 9f9a77fe00b449f617a8cfc832ee82c3d66c404b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 May 2020 16:26:18 +0200 Subject: Add a changelog for 8.11.2. --- .../01-kernel/11972-fix-require-in-section.rst | 6 --- ...12045-missing-reduction-in-using-ind-scheme.rst | 5 -- ...master+fix12152-locating-error-atomic-level.rst | 6 --- .../12070-native-compiler-disabled.rst | 5 -- doc/changelog/09-coqide/12060-ide-disable-csd.rst | 6 --- .../12068-master+coqide-completion-no-matched.rst | 5 -- ...12106-master+coqide-style-apply-all-windows.rst | 5 -- doc/sphinx/changes.rst | 53 ++++++++++++++++++++++ 8 files changed, 53 insertions(+), 38 deletions(-) delete mode 100644 doc/changelog/01-kernel/11972-fix-require-in-section.rst delete mode 100644 doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst delete mode 100644 doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst delete mode 100644 doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst delete mode 100644 doc/changelog/09-coqide/12060-ide-disable-csd.rst delete mode 100644 doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst delete mode 100644 doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst diff --git a/doc/changelog/01-kernel/11972-fix-require-in-section.rst b/doc/changelog/01-kernel/11972-fix-require-in-section.rst deleted file mode 100644 index 7a2fa9185f..0000000000 --- a/doc/changelog/01-kernel/11972-fix-require-in-section.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Using :cmd:`Require` inside a section caused an anomaly when closing - the section. (`#11972 `_, by - Gaëtan Gilbert, fixing `#11783 - `_, reported by Attila - Boros). diff --git a/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst deleted file mode 100644 index 7af2b4d97b..0000000000 --- a/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Anomaly with induction schemes whose conclusion is not normalized - (`#12116 `_, - by Hugo Herbelin; fixes - `#12045 `_) diff --git a/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst deleted file mode 100644 index dc438f151e..0000000000 --- a/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Loss of location of some tactic errors - (`#12223 `_, - by Hugo Herbelin; fixes - `#12152 `_ and - `#12255 `_). diff --git a/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst b/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst deleted file mode 100644 index 0f30b5f5e8..0000000000 --- a/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Ignore -native-compiler option when built without native compute - support. - (`#12070 `_, - by Pierre Roux). diff --git a/doc/changelog/09-coqide/12060-ide-disable-csd.rst b/doc/changelog/09-coqide/12060-ide-disable-csd.rst deleted file mode 100644 index b61ab26007..0000000000 --- a/doc/changelog/09-coqide/12060-ide-disable-csd.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - CoqIDE now uses native window frames by default on Windows. - The GTK window frames can be restored by setting the `GTK_CSD` environment variable to `1` - (`#12060 `_, - fixes `#11080 `_, - by Attila Gáspár). diff --git a/doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst b/doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst deleted file mode 100644 index dbb4bdecab..0000000000 --- a/doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - New patch presumably fixing the random Coq 8.11 segfault issue with CoqIDE completion - (`#12068 `_, - by Hugo Herbelin, presumably fixing - `#11943 `_). diff --git a/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst b/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst deleted file mode 100644 index 6b1148a9a8..0000000000 --- a/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Highlighting style consistently applied to all three buffers of CoqIDE - (`#12106 `_, - by Hugo Herbelin; fixes - `#11506 `_). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 453b8597f9..5954ded67f 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -701,6 +701,59 @@ Changes in 8.11.1 (`#11329 `_, by Hugo Herbelin, fixes `#11114 `_). +Changes in 8.11.2 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Fixed:** + Using :cmd:`Require` inside a section caused an anomaly when closing + the section. (`#11972 `_, by + Gaëtan Gilbert, fixing `#11783 + `_, reported by Attila + Boros). + +**Tactics** + +- **Fixed:** + Anomaly with induction schemes whose conclusion is not normalized + (`#12116 `_, + by Hugo Herbelin; fixes + `#12045 `_) +- **Fixed:** + Loss of location of some tactic errors + (`#12223 `_, + by Hugo Herbelin; fixes + `#12152 `_ and + `#12255 `_). + +**Commands and options** + +- **Changed:** + Ignore -native-compiler option when built without native compute + support. + (`#12070 `_, + by Pierre Roux). + +**CoqIDE** + +- **Changed:** + CoqIDE now uses native window frames by default on Windows. + The GTK window frames can be restored by setting the `GTK_CSD` environment variable to `1` + (`#12060 `_, + fixes `#11080 `_, + by Attila Gáspár). +- **Fixed:** + New patch presumably fixing the random Coq 8.11 segfault issue with CoqIDE completion + (`#12068 `_, + by Hugo Herbelin, presumably fixing + `#11943 `_). +- **Fixed:** + Highlighting style consistently applied to all three buffers of CoqIDE + (`#12106 `_, + by Hugo Herbelin; fixes + `#11506 `_). + Version 8.10 ------------ -- cgit v1.2.3