aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-05-14 16:26:18 +0200
committerPierre-Marie Pédrot2020-05-14 16:26:18 +0200
commit9f9a77fe00b449f617a8cfc832ee82c3d66c404b (patch)
treefcc07415e1c7767ebe53511620ebb23ef225e176
parent8dd5c47007817c104d57a449409a6b9c6f8ef12e (diff)
Add a changelog for 8.11.2.
-rw-r--r--doc/changelog/01-kernel/11972-fix-require-in-section.rst6
-rw-r--r--doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst5
-rw-r--r--doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst6
-rw-r--r--doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst5
-rw-r--r--doc/changelog/09-coqide/12060-ide-disable-csd.rst6
-rw-r--r--doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst5
-rw-r--r--doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst5
-rw-r--r--doc/sphinx/changes.rst53
8 files changed, 53 insertions, 38 deletions
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 <https://github.com/coq/coq/pull/11972>`_, by
- Gaëtan Gilbert, fixing `#11783
- <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/12116>`_,
- by Hugo Herbelin; fixes
- `#12045 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/12223>`_,
- by Hugo Herbelin; fixes
- `#12152 <https://github.com/coq/coq/pull/12152>`_ and
- `#12255 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/12060>`_,
- fixes `#11080 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/12068>`_,
- by Hugo Herbelin, presumably fixing
- `#11943 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/12106>`_,
- by Hugo Herbelin; fixes
- `#11506 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/11329>`_,
by Hugo Herbelin, fixes `#11114 <https://github.com/coq/coq/pull/11114>`_).
+Changes in 8.11.2
+~~~~~~~~~~~~~~~~~
+
+**Kernel**
+
+- **Fixed:**
+ Using :cmd:`Require` inside a section caused an anomaly when closing
+ the section. (`#11972 <https://github.com/coq/coq/pull/11972>`_, by
+ Gaëtan Gilbert, fixing `#11783
+ <https://github.com/coq/coq/issues/11783>`_, reported by Attila
+ Boros).
+
+**Tactics**
+
+- **Fixed:**
+ Anomaly with induction schemes whose conclusion is not normalized
+ (`#12116 <https://github.com/coq/coq/pull/12116>`_,
+ by Hugo Herbelin; fixes
+ `#12045 <https://github.com/coq/coq/pull/12045>`_)
+- **Fixed:**
+ Loss of location of some tactic errors
+ (`#12223 <https://github.com/coq/coq/pull/12223>`_,
+ by Hugo Herbelin; fixes
+ `#12152 <https://github.com/coq/coq/pull/12152>`_ and
+ `#12255 <https://github.com/coq/coq/pull/12255>`_).
+
+**Commands and options**
+
+- **Changed:**
+ Ignore -native-compiler option when built without native compute
+ support.
+ (`#12070 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/12060>`_,
+ fixes `#11080 <https://github.com/coq/coq/issues/11080>`_,
+ by Attila Gáspár).
+- **Fixed:**
+ New patch presumably fixing the random Coq 8.11 segfault issue with CoqIDE completion
+ (`#12068 <https://github.com/coq/coq/pull/12068>`_,
+ by Hugo Herbelin, presumably fixing
+ `#11943 <https://github.com/coq/coq/pull/11943>`_).
+- **Fixed:**
+ Highlighting style consistently applied to all three buffers of CoqIDE
+ (`#12106 <https://github.com/coq/coq/pull/12106>`_,
+ by Hugo Herbelin; fixes
+ `#11506 <https://github.com/coq/coq/pull/11506>`_).
+
Version 8.10
------------