diff options
| author | Théo Zimmermann | 2020-05-27 16:34:55 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-27 16:34:55 +0200 |
| commit | f69bb333e8ef78f0aadb6c6fce56f5a465dde379 (patch) | |
| tree | 2a79ced56338bb3a9aa275aa7c3078338fe0ad4d /doc/sphinx | |
| parent | 29d1594b355a41ae89b0cf4d5318ca767be43f43 (diff) | |
Add more changelog entries which have been backported to v8.12.
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/changes.rst | 13 |
1 files changed, 13 insertions, 0 deletions
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 ^^^^^^ |