Add more changelog entries which have been backported to v8.12.

3 files changed, 13 insertions, 12 deletions

diff --git a/doc/changelog/04-tactics/12366-fix-exists.rst b/doc/changelog/04-tactics/12366-fix-exists.rst
deleted file mode 100644
index 6d976ff562..0000000000
--- a/doc/changelog/04-tactics/12366-fix-exists.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- **Changed:**
-  When using :tacn:`exists` or :tacn:`eexists` with multiple arguments,
-  the evaluation of arguments and applications of constructors are now interleaved.
-  This improves unification in some cases
-  (`#12366 <https://github.com/coq/coq/pull/12366>`_,
-  fixes `#12365 <https://github.com/coq/coq/issues/12365>`_,
-  by Attila Gáspár).
diff --git a/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst b/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst
deleted file mode 100644
index 4e5406ad4d..0000000000
--- a/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  ``make pretty-timed-diff`` no longer raises Python exceptions in the rare
-  corner case where the log of times contains no files (`#12388
-  <https://github.com/coq/coq/pull/12388>`_, fixes `#12387
-  <https://github.com/coq/coq/pull/12387>`_, by Jason Gross).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 7ae1a80eba..72f0fdf4c5 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -242,6 +242,13 @@ Tactics
   arguments should be omitted. Rare source of incompatibility
   (`#12326 <https://github.com/coq/coq/pull/12326>`_,
   by Pierre Courtieu).
+- **Changed:**
+  When using :tacn:`exists` or :tacn:`eexists` with multiple arguments,
+  the evaluation of arguments and applications of constructors are now interleaved.
+  This improves unification in some cases
+  (`#12366 <https://github.com/coq/coq/pull/12366>`_,
+  fixes `#12365 <https://github.com/coq/coq/issues/12365>`_,
+  by Attila Gáspár).
 - **Removed:**
   Undocumented ``omega with``.  Using :tacn:`lia` is the recommended
   replacement, although the old semantics of ``omega with *`` can also
@@ -638,6 +645,12 @@ Tools
   coqchk incorrectly reporting names from opaque modules as axioms
   (`#12076 <https://github.com/coq/coq/pull/12076>`_,
   by Pierre Roux; fixes `#5030 <https://github.com/coq/coq/issues/5030>`_).
+- **Fixed:**
+  coq_makefile-generated ``Makefile``\s ``pretty-timed-diff`` target
+  no longer raises Python exceptions in the rare corner case where the
+  log of times contains no files (`#12388
+  <https://github.com/coq/coq/pull/12388>`_, fixes `#12387
+  <https://github.com/coq/coq/pull/12387>`_, by Jason Gross).
 
 CoqIDE
 ^^^^^^