Merge PR #12460: Add remaining 8.12+beta1 changelog entries.

Reviewed-by: ejgallego

1 files changed, 10 insertions, 0 deletions

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 68ab36a5ff..0f2fce522a 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