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/changelog/04-tactics/12366-fix-exists.rst | 7 ------- .../12388-fix-timing-diff-0s.rst | 5 ----- doc/sphinx/changes.rst | 13 +++++++++++++ 3 files changed, 13 insertions(+), 12 deletions(-) delete mode 100644 doc/changelog/04-tactics/12366-fix-exists.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst 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 `_, - fixes `#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 - `_, fixes `#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 `_, 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 `_, + fixes `#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 `_, by Pierre Roux; fixes `#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 + `_, fixes `#12387 + `_, by Jason Gross). CoqIDE ^^^^^^ -- cgit v1.2.3