Move new entries in 8.11.0 changelog.

8 files changed, 39 insertions, 33 deletions

diff --git a/doc/changelog/01-kernel/11081-native-cleanup.rst b/doc/changelog/01-kernel/11081-native-cleanup.rst
deleted file mode 100644
index b3e3a78b96..0000000000
--- a/doc/changelog/01-kernel/11081-native-cleanup.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Changed:** the native compilation (:tacn:`native_compute`) now
-  creates a directory to contain temporary files instead of putting
-  them in the root of the system temporary directory. (`#11081
-  <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/01-kernel/11422-Setplus2.rst b/doc/changelog/01-kernel/11422-Setplus2.rst
deleted file mode 100644
index cc174358cc..0000000000
--- a/doc/changelog/01-kernel/11422-Setplus2.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Fixed:**
-  The type of :g:`Set+1` would be computed to be itself, leading to a proof of False.
-  (`#11422 <https://github.com/coq/coq/pull/11422>`_,
-  by Gaëtan Gilbert).
diff --git a/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst b/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst
deleted file mode 100644
index a43e950bff..0000000000
--- a/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Deprecated:**
-  The `-load-ml-source` and `-load-ml-object` command line options
-  have been deprecated; their use was very limited, you can achieve the same adding
-  additional object files in the linking step or by using a plugin.
-  (`#11428 <https://github.com/coq/coq/pull/11428>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst
deleted file mode 100644
index 97f456036d..0000000000
--- a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Deprecated:**
-  The ``-quick`` command is renamed to ``-vio``, for consistency with the new ``-vos`` and ``-vok`` flags. Usage of ``-quick`` is now deprecated.
-  (`#11280 <https://github.com/coq/coq/pull/11280>`_,
-  by charguer).
diff --git a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst b/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst
deleted file mode 100644
index 10952c6b2c..0000000000
--- a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints
-  commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_,
-  fixes `#11353 <https://github.com/coq/coq/issues/11353>`_,
-  by Karl Palmskog).
diff --git a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst b/doc/changelog/09-coqide/11400-gtk-ide-completion.rst
deleted file mode 100644
index 2dc3992b9c..0000000000
--- a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  CoqIDE now uses the GtkSourceView native implementation of
-  the autocomplete mechanism.
-  (`#11400 <https://github.com/coq/coq/pull/11400>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst b/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst
deleted file mode 100644
index 3e1f1e02a4..0000000000
--- a/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Removed:**
-  Export of module ``RList`` in ``Ranalysis.v`` and ``Ranalysis_reg.v``. Module ``RList`` is still there but must be imported explicitly where required.
-  (`#11396 <https://github.com/coq/coq/pull/11396>`_,
-  by Michael Soegtrop).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index d1ffb4bbdb..473015dea0 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -519,10 +519,17 @@ Changes in 8.11.0
 
 **Kernel**
 
+- **Changed:** the native compilation (:tacn:`native_compute`) now
+  creates a directory to contain temporary files instead of putting
+  them in the root of the system temporary directory (`#11081
+  <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert).
 - **Fixed:** `#11360 <https://github.com/issues/11360>`_.
   Broken section closing when a template polymorphic inductive type depends on
   a section variable through its parameters (`#11361
   <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert).
+- **Fixed:** The type of :g:`Set+1` would be computed to be itself,
+  leading to a proof of False (`#11422
+  <https://github.com/coq/coq/pull/11422>`_, by Gaëtan Gilbert).
 
 **Specification language, type inference**
 
@@ -574,20 +581,51 @@ Changes in 8.11.0
 **Tactic language**
 
 - **Fixed:**
-  Syntax of tactic `cofix ... with ...` was broken from Coq 8.10.
+  Syntax of tactic `cofix ... with ...` was broken from Coq 8.10
   (`#11241 <https://github.com/coq/coq/pull/11241>`_,
   by Hugo Herbelin).
 
+**Commands and options**
+
+- **Deprecated:** The `-load-ml-source` and `-load-ml-object` command
+  line options have been deprecated; their use was very limited, you
+  can achieve the same by adding object files in the linking step or
+  by using a plugin (`#11428
+  <https://github.com/coq/coq/pull/11428>`_, by Emilio Jesus Gallego
+  Arias).
+
 **Tools**
 
 - **Fixed:**
   ``coqtop --version`` was broken when called in the middle of an installation process
   (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing
   `#11254 <https://github.com/coq/coq/pull/11254>`_).
+- **Deprecated:** The ``-quick`` command is renamed to ``-vio``, for
+  consistency with the new ``-vos`` and ``-vok`` flags. Usage of
+  ``-quick`` is now deprecated (`#11280
+  <https://github.com/coq/coq/pull/11280>`_, by Arthur Charguéraud).
 - **Fixed:**
   ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable
   together with an unpacked (``mllib``) plugin. (`#11357
   <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert).
+- **Fixed:**
+  ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints
+  commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_,
+  fixes `#11353 <https://github.com/coq/coq/issues/11353>`_,
+  by Karl Palmskog).
+
+**CoqIDE**
+
+- **Changed:** CoqIDE now uses the GtkSourceView native implementation
+  of the autocomplete mechanism (`#11400
+  <https://github.com/coq/coq/pull/11400>`_, by Pierre-Marie Pédrot).
+
+**Standard library**
+
+- **Removed:** Export of module :g:`RList` in :g:`Ranalysis` and
+  :g:`Ranalysis_reg`. Module :g:`RList` is still there but must be
+  imported explicitly where required (`#11396
+  <https://github.com/coq/coq/pull/11396>`_, by Michael Soegtrop).
 
 **Infrastructure and dependencies**