From 3120838ba24da0b978ba890a7724827709f8ac26 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 22 Jan 2020 19:44:03 +0100 Subject: Minor tweaks to the 8.11 changelog. --- doc/sphinx/changes.rst | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 294f121cf8..1dac3c7baf 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -60,15 +60,15 @@ of |Coq| and affected releases. See the `Changes in 8.11+beta1`_ section and following sections for the detailed list of changes, including potentially breaking changes marked with **Changed**. -Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael -Soegtrop, Théo Zimmermann worked on maintaining and improving the -continuous integration system and package building infrastructure. - Coq's documentation is available at https://coq.github.io/doc/v8.11/api (documentation of the ML API), https://coq.github.io/doc/v8.11/refman (reference manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of the standard library). +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop, Théo Zimmermann worked on maintaining and improving the +continuous integration system and package building infrastructure. + The OPAM repository for |Coq| packages has been maintained by Guillaume Claret, Karl Palmskog, Matthieu Sozeau, Enrico Tassi with contributions from many users. A list of packages is available at @@ -566,7 +566,8 @@ Changes in 8.11.0 `_, fixes `#10971 `_, by Jason Gross) - **Fixed:** - Efficiency regression introduced by PR `#9725 `_ + Efficiency regression of :tacn:`lia` introduced in 8.10 + by PR `#9725 `_ (`#11263 `_, fixes `#11063 `_, and `#11242 `_, @@ -579,14 +580,14 @@ Changes in 8.11.0 by Emilio Jesus Gallego Arias). - **Fixed** For compatibility reasons, in 8.11, :tacn:`zify` does not support :g:`Z.pow_pos` by default. - It can be enabled by loading explicitly the module :g:`ZifyPow`. + It can be enabled by loading explicitly the module :g:`ZifyPow` (`#11430 `_ by Frédéric Besson fixes `#11191 `_). **Tactic language** - **Fixed:** - Syntax of tactic `cofix ... with ...` was broken from Coq 8.10 + Syntax of tactic `cofix ... with ...` was broken since Coq 8.10 (`#11241 `_, by Hugo Herbelin). @@ -611,7 +612,7 @@ Changes in 8.11.0 `_, by Arthur Charguéraud). - **Fixed:** ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable - together with an unpacked (``mllib``) plugin. (`#11357 + together with an unpacked (``mllib``) plugin (`#11357 `_, by Gaëtan Gilbert). - **Fixed:** ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints -- cgit v1.2.3 From c78e47e744ae6c8a1b410fa952740cdfc3bd1c3b Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 23 Jan 2020 08:44:48 +0100 Subject: Add missing 'and'. Co-Authored-By: Jim Fehrle --- doc/sphinx/changes.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 1dac3c7baf..c30e90a1f3 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -66,11 +66,11 @@ manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of the standard library). Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael -Soegtrop, Théo Zimmermann worked on maintaining and improving the +Soegtrop and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure. The OPAM repository for |Coq| packages has been maintained by -Guillaume Claret, Karl Palmskog, Matthieu Sozeau, Enrico Tassi with +Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. -- cgit v1.2.3 From 1d88962aaaa5f8977bb343b1d01073d65cbb1434 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 23 Jan 2020 09:45:01 +0100 Subject: More minor tweaks to the 8.11 changelog. Co-Authored-By: Jim Fehrle --- doc/sphinx/changes.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index c30e90a1f3..6d9979a704 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -574,13 +574,13 @@ Changes in 8.11.0 and `#11270 `_, by Frédéric Besson). - **Deprecated:** The undocumented ``omega with`` tactic variant has been deprecated. - Using :tacn:`lia` is the recommended replacement, tho the old semantics + Using :tacn:`lia` is the recommended replacement, though the old semantics of ``omega with *`` can be recovered with ``zify; omega`` (`#11337 `_, by Emilio Jesus Gallego Arias). - **Fixed** For compatibility reasons, in 8.11, :tacn:`zify` does not support :g:`Z.pow_pos` by default. - It can be enabled by loading explicitly the module :g:`ZifyPow` + It can be enabled by explicitly loading the module :g:`ZifyPow` (`#11430 `_ by Frédéric Besson fixes `#11191 `_). @@ -636,7 +636,7 @@ Changes in 8.11.0 **Infrastructure and dependencies** - **Added:** - Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` + Build date can now be overridden by setting the `SOURCE_DATE_EPOCH` environment variable (`#11227 `_, by Bernhard M. Wiedemann). -- cgit v1.2.3