From f69bb333e8ef78f0aadb6c6fce56f5a465dde379 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 27 May 2020 16:34:55 +0200
Subject: Add more changelog entries which have been backported to v8.12.

---
 doc/sphinx/changes.rst | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'doc/sphinx')

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
 ^^^^^^
-- 
cgit v1.2.3