Add remaining 8.12+beta1 changelog entries.

3 files changed, 10 insertions, 10 deletions

diff --git a/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst
deleted file mode 100644
index 8f126c5b6f..0000000000
--- a/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Case of an anomaly in trying to infer the return clause of an ill-typed :g:`match`
-  (`#12422 <https://github.com/coq/coq/pull/12422>`_,
-  fixes `#12418 <https://github.com/coq/coq/pull/12418>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/07-commands-and-options/11972-fix-require-in-section.rst b/doc/changelog/07-commands-and-options/11972-fix-require-in-section.rst
deleted file mode 100644
index 7e34c4a0ff..0000000000
--- a/doc/changelog/07-commands-and-options/11972-fix-require-in-section.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:** The warning when using :cmd:`Require` inside a section
-  moved from the ``deprecated`` category to the ``fragile`` category,
-  because there is no plan to remove the functionality at this time.
-  (`#11972 <https://github.com/coq/coq/pull/11972>`_, by Gaëtan
-  Gilbert).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 72f0fdf4c5..6242833cda 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -76,6 +76,11 @@ Specification language, type inference
   Anomaly which could be raised when printing binders with implicit types
   (`#12323 <https://github.com/coq/coq/pull/12323>`_,
   by Hugo Herbelin; fixes `#12322 <https://github.com/coq/coq/pull/12322>`_).
+- **Fixed:**
+  Case of an anomaly in trying to infer the return clause of an ill-typed :g:`match`
+  (`#12422 <https://github.com/coq/coq/pull/12422>`_,
+  fixes `#12418 <https://github.com/coq/coq/pull/12418>`_,
+  by Hugo Herbelin).
 
 Notations
 ^^^^^^^^^
@@ -440,6 +445,11 @@ Commands
   Several commands (:cmd:`Search`, :cmd:`About`, ...) now print the
   implicit arguments in brackets when printing types (`#11795
   <https://github.com/coq/coq/pull/11795>`_, by Simon Boulier).
+- **Changed:** The warning when using :cmd:`Require` inside a section
+  moved from the ``deprecated`` category to the ``fragile`` category,
+  because there is no plan to remove the functionality at this time
+  (`#11972 <https://github.com/coq/coq/pull/11972>`_, by Gaëtan
+  Gilbert).
 - **Changed:**
   :cmd:`Redirect` now obeys the :opt:`Printing Width` and
   :opt:`Printing Depth` options