Documentation of branch “master” at 8b16a4e2

master/refman/_sources/changes.rst.txt

@@ -14,7 +14,113 @@ Version 8.19
 Summary of changes
 ~~~~~~~~~~~~~~~~~~
 
-TODO
+Coq version 8.19 extends the kernel universe polymorphism to
+polymorphism over sorts (e.g. `Prop`, `SProp`) along with a few new
+features, a host of improvements to the notation system, the Ltac2
+standard library, and the removal of some standard library files after
+a long deprecation period.
+
+We highlight some of the most impactful changes here:
+
+  - :ref:`sort-polymorphism` makes it possible to share common constructs
+    over `Type` `Prop` and `SProp`.
+
+  - The notation :g:`term%_scope` to set a scope only temporarily
+    (in addition to :g:`term%scope` for opening a
+    scope applying to all subterms).
+
+  - :tacn:`lazy`, :tacn:`simpl`, :tacn:`cbn` and :tacn:`cbv` and the associated :cmd:`Eval`
+    and :tacn:`eval` reductions learned to do head reduction when given flag `head`.
+
+  - :ref:`New Ltac2 APIs <819Ltac2>`, improved Ltac2 `exact` and
+    dynamic building of Ltac2 term patterns.
+
+  - New performance evaluation facilities: :cmd:`Instructions` to
+    count CPU instructions used by a command (Linux only) and
+    :ref:`profiling` system to produce trace files.
+
+  - New command :cmd:`Attributes` to assign attributes such as
+    :attr:`deprecated` to a library file.
+
+Notable breaking changes:
+
+  - :tacn:`replace` with `by tac` does not automatically attempt to solve
+    the generated equality subgoal using the hypotheses.
+    Use `by first [assumption | symmetry;assumption | tac]`
+    if you need the previous behaviour.
+
+  - :ref:`Removed old deprecated files <819Stdlib>` from the standard library.
+
+See the `Changes in 8.19.0`_ section below for the detailed list of changes,
+including potentially breaking changes marked with **Changed**.
+Coq's `reference manual for 8.19 <https://coq.github.io/doc/v8.19/refman>`_,
+`documentation of the 8.19 standard library <https://coq.github.io/doc/v8.19/stdlib>`_
+and `developer documentation of the 8.19 ML API <https://coq.github.io/doc/v8.19/api>`_
+are also available.
+
+Maxime Dénès and Thierry Martinez with support from Erik Martin-Dorel
+and Théo Zimmermann moved the CI away from `gitlab.com <http://gitlab.com>`_
+to use Inria supported runner machines through
+`gitlab.inria.fr <https://gitlab.inria.fr>`_.
+
+Théo Zimmermann with help from Ali Caglayan and Jason Gross maintained
+`coqbot <https://github.com/coq/bot>`_ used to run Coq's CI and other
+pull request management tasks.
+
+Jason Gross maintained the `bug minimizer <https://github.com/JasonGross/coq-tools>`_
+and its `automatic use through coqbot <https://github.com/coq/coq/wiki/Coqbot-minimize-feature>`_.
+
+Jaime Arias and Erik Martin-Dorel maintained the
+`Coq Docker images <https://hub.docker.com/r/coqorg/coq>`_
+and Cyril Cohen, Vincent Laporte, Pierre Roux and Théo Zimmermann
+maintained the `Nix toolbox <https://github.com/coq-community/coq-nix-toolbox>`_
+used by many Coq projects for continuous integration.
+
+Ali Caglayan, Emilio Jesús Gallego Arias, Rudi Grinberg and
+Rodolphe Lepigre maintained the
+`Dune build system for OCaml and Coq <https://github.com/ocaml/dune/>`_
+used to build Coq itself and many Coq projects.
+
+The opam repository for Coq packages has been maintained by
+Guillaume Claret, Guillaume Melquiond, Karl Palmskog and Enrico Tassi with
+contributions from many users. A list of packages is `available on the Coq website <https://coq.inria.fr/coq-package-index>`_.
+
+Our current maintainers are Yves Bertot, Frédéric Besson, Ana Borges,
+Ali Caglayan, Tej Chajed, Cyril Cohen, Pierre Corbineau, Pierre
+Courtieu, Andres Erbsen, Jim Fehrle, Julien Forest, Emilio Jesús
+Gallego Arias, Gaëtan Gilbert, Georges Gonthier, Benjamin Grégoire,
+Jason Gross, Hugo Herbelin, Vincent Laporte, Olivier Laurent, Assia
+Mahboubi, Kenji Maillard, Guillaume Melquiond, Pierre-Marie Pédrot,
+Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria,
+Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico Tassi,
+Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann. See the
+`Coq Team face book <https://coq.inria.fr/coq-team.html>`_ page for
+more details.
+
+The 40 contributors to the 8.19 version are:
+quarkcool, Khalid Abdullah, Tanaka Akira, Isaac van Bakel,
+Frédéric Besson, Lasse Blaauwbroek, Ana Borges, Ali Caglayan, Nikolaos
+Chatzikonstantinou, Maxime Dénès, Andrej Dudenhefner, Andres Erbsen,
+Jim Fehrle, Gaëtan Gilbert, Jason Gross, Stefan Haan, Hugo Herbelin,
+Emilio Jesús Gallego Arias, Pierre Jouvelot, Ralf Jung, Jan-Oliver
+Kaiser, Robbert Krebbers, Jean-Christophe Léchenet, Rodolphe Lepigre,
+Yann Leray, Yishuai Li, Guillaume Melquiond, Guillaume
+Munch-Maccagnoni, Sotaro Okada, Karl Palmskog, Pierre-Marie Pédrot, Jim Portegies,
+Pierre Rousselin, Pierre Roux, Michael Soegtrop, David Swasey, Enrico
+Tassi, Shengyi Wang and Théo Zimmermann.
+
+The Coq community at large helped improve this new version via
+the GitHub issue and pull request system, the [email protected] mailing list,
+the `Discourse forum <https://coq.discourse.group/>`_ and the
+`Coq Zulip chat <https://coq.zulipchat.com>`_.
+
+Version 8.19's development spanned 4 months from the release of Coq 8.18.0
+(6 months since the branch for 8.18.0).
+Gaëtan Gilbert and Matthieu Sozeau are the release managers of Coq 8.19.
+This release is the result of 285 merged PRs, closing 70 issues.
+
+| Nantes, January 2024
+| Gaëtan Gilbert for the Coq development team
 
 Changes in 8.19.0
 ~~~~~~~~~~~~~~~~~
@@ -210,6 +316,12 @@ Tactics
   form `0 <= _ < _` for better cleanup in ``zify``
   (`#17984 <https://github.com/coq/coq/pull/17984>`_,
   by Jason Gross).
+- **Changed:**
+  :tacn:`simpl` now refolds applied constants unfolding to reducible
+  fixpoints into the original constant even when this constant
+  would become partially applied
+  (`#17991 <https://github.com/coq/coq/pull/17991>`_,
+  by Hugo Herbelin).
 - **Added:**
   Ltac2 tactic `Std.resolve_tc` to resolve typeclass evars appearing in a given term
   (`#13071 <https://github.com/coq/coq/pull/13071>`_,
@@ -282,19 +394,15 @@ Tactics
 
 Ltac language
 ^^^^^^^^^^^^^
-- **Changed:**
-  :tacn:`simpl` now refolds applied constants unfolding to reducible
-  fixpoints into the original constant even when this constant
-  would become partially applied
-  (`#17991 <https://github.com/coq/coq/pull/17991>`_,
-  by Hugo Herbelin).
 - **Fixed:**
   Fix broken "r <num>" and "r <string>" commands in the coqtop
   Ltac debugger, which also affected the Proof General Ltac debugger
   (`#18068 <https://github.com/coq/coq/pull/18068>`_,
   fixes `#18067 <https://github.com/coq/coq/issues/18067>`_,
   by Jim Fehrle).
 
+.. _819Ltac2:
+
 Ltac2 language
 ^^^^^^^^^^^^^^
 - **Changed:**
@@ -443,6 +551,8 @@ Command-line tools
   (`#18165 <https://github.com/coq/coq/pull/18165>`_,
   by Rodolphe Lepigre).
 
+.. _819Stdlib:
+
 Standard library
 ^^^^^^^^^^^^^^^^
 

master/refman/addendum/canonical-structures.html

@@ -990,50 +990,50 @@
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-16">Version 8.16</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id462">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id468">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-16-0">Changes in 8.16.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-16-1">Changes in 8.16.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-15">Version 8.15</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id625">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id631">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-15-0">Changes in 8.15.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-15-1">Changes in 8.15.1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-15-2">Changes in 8.15.2</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-14">Version 8.14</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id853">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id859">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-14-0">Changes in 8.14.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-14-1">Changes in 8.14.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-13">Version 8.13</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1049">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1055">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-13-beta1">Changes in 8.13+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-13-0">Changes in 8.13.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-13-1">Changes in 8.13.1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-13-2">Changes in 8.13.2</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-12">Version 8.12</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1213">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1219">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-12-beta1">Changes in 8.12+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-12-0">Changes in 8.12.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-12-1">Changes in 8.12.1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-12-2">Changes in 8.12.2</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-11">Version 8.11</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1519">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1525">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-11-beta1">Changes in 8.11+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-11-0">Changes in 8.11.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-11-1">Changes in 8.11.1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-11-2">Changes in 8.11.2</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-10">Version 8.10</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1657">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1663">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#other-changes-in-8-10-beta1">Other changes in 8.10+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-10-beta2">Changes in 8.10+beta2</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-10-beta3">Changes in 8.10+beta3</a></li>
@@ -1043,22 +1043,22 @@
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-9">Version 8.9</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1804">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1810">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-9-beta1">Details of changes in 8.9+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-8-0">Changes in 8.8.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-8-1">Changes in 8.8.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-8">Version 8.8</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1806">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1812">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-8-beta1">Details of changes in 8.8+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-8-0">Details of changes in 8.8.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-8-1">Details of changes in 8.8.1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-8-2">Details of changes in 8.8.2</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-7">Version 8.7</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1807">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1813">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#potential-compatibility-issues">Potential compatibility issues</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-7-beta1">Details of changes in 8.7+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-7-beta2">Details of changes in 8.7+beta2</a></li>
@@ -1068,16 +1068,16 @@
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-6">Version 8.6</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1808">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1814">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#potential-sources-of-incompatibilities">Potential sources of incompatibilities</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-6beta1">Details of changes in 8.6beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-6">Details of changes in 8.6</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-6-1">Details of changes in 8.6.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-5">Version 8.5</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1809">Summary of changes</a></li>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1810">Potential sources of incompatibilities</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1815">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1816">Potential sources of incompatibilities</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-5beta1">Details of changes in 8.5beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-5beta2">Details of changes in 8.5beta2</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-5beta3">Details of changes in 8.5beta3</a></li>
@@ -1088,32 +1088,32 @@
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-4">Version 8.4</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1811">Summary of changes</a></li>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1813">Potential sources of incompatibilities</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1817">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1819">Potential sources of incompatibilities</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-4beta">Details of changes in 8.4beta</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-4beta2">Details of changes in 8.4beta2</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-4">Details of changes in 8.4</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-3">Version 8.3</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1814">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1820">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes">Details of changes</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-2">Version 8.2</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1815">Summary of changes</a></li>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1816">Details of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1821">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1822">Details of changes</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-1">Version 8.1</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1817">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1823">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-1beta">Details of changes in 8.1beta</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-1gamma">Details of changes in 8.1gamma</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-1">Details of changes in 8.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-0">Version 8.0</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1818">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1824">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-0beta-old-syntax">Details of changes in 8.0beta old syntax</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-0beta-new-syntax">Details of changes in 8.0beta new syntax</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-0">Details of changes in 8.0</a></li>