Quelle changes.rst Sprache: unbekannt

.. _changes:

--------------
Recent changes
--------------

.. ifconfig:: not is_a_released_version

   .. include:: ../unreleased.rst

Version 9.1
-----------

.. contents::
   :local:
   :depth: 1

Summary of changes
~~~~~~~~~~~~~~~~~~

We highlight some of the most impactful changes here:

- fixed incorrect guard checking leading to inconsistencies (multiple PRs)

- sort polymorphic universe instances :ref:`should now be written <91sortpolysyntax>`
  as `@{s ; u}` instead of `@{s | u}`

- :ref:`fixed <91ltac2notationfix>` handling of notation variables for ltac2 in notations
  (i.e. `Notation "'foo' x" := ltac2:(...)`)

- :ref:`Support <91refinedef>` for :attr:`refine` attribute in :cmd:`Definition`

- Rocq can be compile-time configured to be :ref:`relocatable <91relocatable>`

- extraction :ref:`handles <91extractsortpoly>` sort polymorphic definitions

See the `Changes in 9.1.0`_ section below for the detailed list of changes,
including potentially breaking changes marked with **Changed**.
Rocq's `reference manual for 9.1 <https://rocq-prover.org/doc/v9.1/refman>`_,
documentation of the 9.1 `corelib <https://rocq-prover.org/doc/v9.1/corelib>`__
and `developer documentation of the 9.1 ML API <https://rocq-prover.org/doc/v9.1/api>`_
are also available.

Théo Zimmermann, with help from Jason Gross and Gaëtan Gilbert, maintained
`coqbot <https://github.com/rocq-prover/bot>`__ used to run Rocq'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/rocq-prover/rocq/wiki/Coqbot-minimize-feature>`__.

Ali Caglayan, Emilio Jesús Gallego Arias, Rudi Grinberg and Rodolphe Lepigre maintained the
`Dune build system for OCaml and Coq/Rocq <https://github.com/ocaml/dune/>`_
used to build the Rocq Prover itself and many Rocq projects.

The `opam repository <https://github.com/coq/opam>`_ for Rocq packages has been maintained by
Guillaume Claret, Guillaume Melquiond, Karl Palmskog, Matthieu Sozeau
and Enrico Tassi with contributions from many users. The up-to-date list
of packages is `available on the Rocq website <https://rocq-prover.org/packages>`_.

Erik Martin-Dorel maintained the
`Rocq Docker images <https://hub.docker.com/r/rocq/rocq-prover>`_ and
the `docker-keeper <https://gitlab.com/erikmd/docker-keeper>`_ compiler
used to build and keep those images up to date (note that the tool is not Rocq specific).
Erik Martin-Dorel and Théo Zimmermann maintained the
`docker-coq-action <https://github.com/coq-community/docker-coq-action>`_
container action (which is applicable to any opam project hosted on GitHub).

Cyril Cohen, Vincent Laporte, Pierre Roux and Théo Zimmermann
maintained the `Nix toolbox <https://github.com/coq-community/coq-nix-toolbox>`_.
The docker-coq-action and the Nix toolbox are used by many Rocq projects for continuous integration.

Rocq 9.1 was made possible thanks to the following 24 reviewers:
Florian Angeletti, Ali Caglayan, Cyril Cohen, Pierre Courtieu, Jim
Fehrle, Gaëtan Gilbert, Jason Gross, Emilio Jesús Gallego Arias,
Jan-Oliver Kaiser, Thomas Lamiaux, Rodolphe Lepigre,
Erik Martin-Dorel, Guillaume Melquiond, Patrick Nicodemus,
Pierre-Marie Pédrot, Pierre Rousselin, Pierre Roux, Gabriel Scherer,
Matthieu Sozeau, Nicolas Tabareau, Enrico Tassi, Théo Winterhalter and
Théo Zimmermann.

See the `Rocq Team <https://rocq-prover.org/rocq-team>`_ page for
more details on Rocq's development teams.

The 45 contributors to the 9.1 version are: Soudant,
ypopovitch, Reynald Affeldt, Wassim Ait-Moussa, David Allsopp,
Christian Benedict Smit, Frédéric Besson, Mathis Bouverot, Ali
Caglayan, Jean Caspar, Benedict Christian Smit, Cyril Cohen, Pierre Courtieu,
Julien Cretin, Jian Fang, Jim Fehrle, Gaëtan Gilbert, Jason Gross,
Dario Halilovic, Hugo Herbelin, Elyes Jemel, Emilio Jesús Gallego
Arias, Jan-Oliver Kaiser, Kacper Korban, Lucie Lahaye, Thomas Lamiaux,
Rodolphe Lepigre, Yann Leray, Kenji Maillard, Erik Martin-Dorel,
Patrick Nicodemus, Charles Norton, Pim Otte, Pierre-Marie Pédrot,
Josselin Poiret, Johann Rosain, Pierre Rousselin, Pierre Roux,
Radosław Rowicki, Benedict Smit, Bastien Sozeau, Matthieu Sozeau,
Nicolas Tabareau, Enrico Tassi and Théo Zimmermann.

The Rocq community at large helped improve this new version via
the GitHub issue and pull request system,
the `Discourse forum <https://discourse.rocq-prover.org>`__ and the
`Rocq Zulip chat <https://rocq-prover.zulipchat.com>`_.

Gaëtan Gilbert and Pierre-Marie Pédrot are the release managers of Rocq 9.1.
This release is the result of 397 merged PRs, closing 56 issues.

| Nantes, September 2025
| Gaëtan Gilbert and Pierre-Marie Pédrot for the Rocq development team

Changes in 9.1.0
~~~~~~~~~~~~~~~~

.. contents::
   :local:

Kernel
^^^^^^

- **Fixed:**
  Guard checking forgot to check non principal arguments of a fixpoint
  for unguarded uses of the fixpoint leading to an inconsistency
  (`#20415 <https://github.com/coq/coq/pull/20415>`_,
  fixes `#20413 <https://github.com/coq/coq/issues/20413>`_,
  by Gaëtan Gilbert).
- **Fixed:**
  inconsistency from incomplete guard checking with nested matches
  (`#20457 <https://github.com/rocq-prover/rocq/pull/20457>`_,
  fixes `#20455 <https://github.com/rocq-prover/rocq/issues/20455>`_,
  by Gaëtan Gilbert).
- **Fixed:**
  inconsistency from incorrect reduction across a fixpoint during guard checking
  (`#20648 <https://github.com/rocq-prover/rocq/pull/20648>`_,
  fixes `#20555 <https://github.com/rocq-prover/rocq/issues/20555>`_,
  by Yann Leray).
- **Fixed:**
  Wrong context management during rewrite rule reduction
  (`#20729 <https://github.com/rocq-prover/rocq/pull/20729>`_,
  fixes `#20728 <https://github.com/rocq-prover/rocq/issues/20728>`_,
  by Yann Leray).
- **Fixed:**
  Fix guard checker making propositional extensionality inconsistent
  (`#21050 <https://github.com/rocq-prover/rocq/pull/21050>`_,
  fixes `#21053 <https://github.com/rocq-prover/rocq/issues/21053>`_,
  by Yann Leray).
- **Fixed:**
  substitution of functor delta-resolvers when strengthening.
  The previous code was only substituting the inner delta resolvers
  and ignoring the codomain of functors. In particular this was generating
  ill-formed constants whose canonical component was pointing to a bound name
  that did not exist in the global environment, leading to an inconsistency
  (`#21057 <https://github.com/rocq-prover/rocq/pull/21057>`_,
  fixes `#21051 <https://github.com/rocq-prover/rocq/issues/21051>`_,
  by Pierre-Marie Pédrot).

Specification language, type inference
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. _91sortpolysyntax:

- **Deprecated:**
  in :ref:`sort polymorphic <sort-polymorphism>` instances, separating sorts from universes using `|` instead of `;` (the later being possible since this version)
  (`#20635 <https://github.com/rocq-prover/rocq/pull/20635>`_,
  by Gaëtan Gilbert).
- **Added:**
  in :ref:`sort polymorphic <sort-polymorphism>` instances, sorts can be separated from universes using `;` instead of `|`.
  This is less ambiguous as `|` is also used to separate universes and constraints when declaring sort polymorphic objects,
  and in such declarations when constraints are unspecified it allows omitting the `|`
  (`Definition foo@{s;u} := ...` instead of `Definition foo@{s|u|+} := ...`)
  (`#20635 <https://github.com/rocq-prover/rocq/pull/20635>`_,
  by Gaëtan Gilbert).
- **Fixed:**
  Anomaly `List.chop` in the presence of projections with not
  enough argument scopes (`#20945
  <https://github.com/rocq-prover/rocq/pull/20945>`_, fixes `#20940
  <https://github.com/rocq-prover/rocq/issues/20940>`_, by Hugo
  Herbelin).
- **Fixed:**
  Anomaly `List.chop` with too many projection parameters in an abbreviation
  (`#20946 <https://github.com/rocq-prover/rocq/pull/20946>`_,
  fixes `#15815 <https://github.com/rocq-prover/rocq/issues/15815>`_,
  by Hugo Herbelin).

Notations
^^^^^^^^^

- **Changed:**
  The `Specif` notations (`exists x : A, P`, `{ x : A | P }`, `{ x : A & P }`, etc)
  locally opens `type_scope` for the second component (`P`).
  This makes eg `{ x & type_1 * type_2 }` work even when `nat_scope` is opened instead of interpreting `*` as peano multiplication
  (`#20294 <https://github.com/coq/coq/pull/20294>`_,
  by Gaëtan Gilbert).
- **Changed:**
  :cmd:`Enable Notation` and :cmd:`Disable Notation` do not take
  effect in deep imports (i.e. when a parent of their origin module is
  imported)
  (`#20484 <https://github.com/rocq-prover/rocq/pull/20484>`_,
  by Gaëtan Gilbert).

Tactics
^^^^^^^

- **Changed:**
  the :tacn:`abstract` tactic now only registers a name
  for the sublemma after the whole tactic block has run,
  i.e. after a dot. In particular, the sublemma cannot
  be accessed by its name while the tactic call has not
  returned
  (`#14937 <https://github.com/coq/coq/pull/14937>`_,
  by Pierre-Marie Pédrot).
- **Changed:**
  the congruence tactic now can handle some dependently typed constructor fields.
  The field's type has to be composed of terms occuring globally or projectable from
  parameters or indices of the inductive type
  (`#19700 <https://github.com/rocq-prover/rocq/pull/19700>`_,
  by Benedict Christian Smit).
- **Changed:**
  setoid rewriting now rewrites under primitive projections.
  In rare cases (see for instance
  `#20575 <https://github.com/rocq-prover/rocq/issues/20575>`_),
  some rewrite that used to accidentally work will now correctly fail
  (`#19811 <https://github.com/rocq-prover/rocq/pull/19811>`_,
  by Josselin Poiret and Pierre-Marie Pédrot).
- **Changed:**
  output of :cmd:`Print Instances` better matches the actual behaviour
  when an instance is declared multiple times with different priorities
  (`#20486 <https://github.com/rocq-prover/rocq/pull/20486>`_,
  by Gaëtan Gilbert).
- **Added:**
  a new :flag:`Rewrite Output Constraints` flag and :ref:`documented <debugging_resolution_issues>` its use
  for debugging typeclass resolution failures in setoid rewriting
  (`#20476 <https://github.com/rocq-prover/rocq/pull/20476>`_,
  by Matthieu Sozeau).

Ltac language
^^^^^^^^^^^^^

- **Changed:**
  :cmd:`Ltac` redefinitions (`Ltac ::=`) understand :attr:`export`.
  Previously :attr:`global` and the default locality meant the redefinition would
  take effect at Require time and when importing any surrounding module.
  Now :attr:`global` means it takes affect at Require time,
  :attr:`export` when the current module (but not its parents) is imported,
  and the default is equivalent to the combination of :attr:`global` and :attr:`export`
  (`#20054 <https://github.com/coq/coq/pull/20054>`_,
  by Gaëtan Gilbert).
- **Changed:**
  :cmd:`Ltac` redefinitions (`Ltac foo ::= ...`) are not undone by
  importing the module containing the original definition.
  To get the previous behaviour, add `Ltac foo ::= orig_def.`
  after the original definition `Ltac foo := orig_def.`
  (`#20391 <https://github.com/coq/coq/pull/20391>`_,
  by Gaëtan Gilbert).
- **Changed:**
  Named goals can now appear in any goal selector list
  (`#20511 <https://github.com/rocq-prover/rocq/pull/20511>`_,
  fixes `#12838 <https://github.com/rocq-prover/rocq/issues/12838>`_,
  by Dario Halilovic).

Ltac2 language
^^^^^^^^^^^^^^

- **Changed:**
  Ltac2 does not depend on the prelude (i.e.  it is compiled with `-noinit`).
  It still depends on `Corelib.Init.Ltac` due to the interoperation with Ltac1
  (`#20387 <https://github.com/rocq-prover/rocq/pull/20387>`_,
  by Gaëtan Gilbert).
- **Changed:**
  the documentation and error messages do not use the term "scope" to describe Ltac2 :ref:`syntactic_classes`
  (`#20504 <https://github.com/rocq-prover/rocq/pull/20504>`_,
  by Gaëtan Gilbert).
- **Changed:**
  :cmd:`Ltac2 Set` only takes effect with shallow imports, i.e.
  `Import Foo` will not run a mutation from (non exported) inner module `Foo.Bar`
  (`#20516 <https://github.com/rocq-prover/rocq/pull/20516>`_,
  by Gaëtan Gilbert).
- **Added:**
  A file `Ltac1CompatNotations` for Ltac2 Notations reproducing Ltac1 parsing of tactics,
  that can be harmful to parsing, and produce bad error messages.
  (`#20569 <https://github.com/rocq-prover/rocq/pull/20569>`_,
  by Thomas Lamiaux).
- **Added:**
  `rename` (in `Ltac1CompatNotations`), `eassumption`, `cycle`, and `exfalso` Ltac2 notations
  (`#20197 <https://github.com/rocq-prover/rocq/pull/20197>`_,
  by Josselin Poiret).
- **Added:**
  ``Ltac2.Constr.is_string``, ``Ltac2.Constr.is_sort``
  (`#20088 <https://github.com/coq/coq/pull/20088>`_,
  by Jason Gross).
- **Added:**
  ``Ltac2.Constr.decompose_app_list``, ``Ltac2.Constr.decompose_app``
  (`#20089 <https://github.com/coq/coq/pull/20089>`_,
  by Jason Gross).
- **Added:**
  ``Ltac2.Option.is_some``, ``Ltac2.Option.is_none``, ``Ltac2.Option.compare``,
  ``Ltac2.Option.join``, ``Ltac2.Option.iter``
  (`#20184 <https://github.com/coq/coq/pull/20184>`_,
  by Jason Gross).
- **Added:**
  `empty` and `add` in `Ltac2.Fresh.Free`, `next` in `Ltac2.Fresh`.
  `Ltac2.Fresh` operations should also be faster
  (`#20220 <https://github.com/coq/coq/pull/20220>`_,
  by Gaëtan Gilbert).
- **Added:**
  Enable use of (open\_)lconstr inside Ltac2 Notation command
  (`#20430 <https://github.com/coq/coq/pull/20430>`_,
  by Pim Otte).
- **Added:**
  API functions for inductive types - `Ind.nparams`, `Ind.nparams_uniform`, `Ind.constructor_nargs`, `Ind.constructor_ndecls`, `Constr.Case.inductive`
  (`#20475 <https://github.com/rocq-prover/rocq/pull/20475>`_,
  fixes `#10940 <https://github.com/rocq-prover/rocq/issues/10940>`_,
  by Patrick Nicodemus).
- **Added:**
  format specifiers `%A` to use unthunked printers and `%m` for already-formatted messages.
  Typically, instead of `printf "foo: %a" (fun () v => print_thing v) v`
  we can now write `printf "foo: %A" print_thing v`
  or `printf "foo: %m" (print_thing v)`
  (`#20498 <https://github.com/rocq-prover/rocq/pull/20498>`_,
  by Gaëtan Gilbert).
- **Added:**
  Ltac2 type for reduction expressions
  (`#20543 <https://github.com/rocq-prover/rocq/pull/20543>`_,
  by Radosław Rowicki, with review of Pierre-Marie Pédrot and Gaëtan Gilbert and Jason Gross).
- **Added:**
  Ported `rewrite_strat` to Ltac2 and added the `Rewrite.Strategy` module for describing rewrite strategies
  (`#20544 <https://github.com/rocq-prover/rocq/pull/20544>`_,
  fixes `#20482 <https://github.com/rocq-prover/rocq/issues/20482>`_,
  by Radosław Rowicki with review of Jason Gross and Pierre-Marie Pédrot and Gaëtan Gilbert).
- **Added:**
  ``Ltac2.Message.empty``
  (`#20547 <https://github.com/coq/coq/pull/20547>`_,
  by Elyes Jemel).
- **Added:**
  conversion tests to Unification - `Unification.conv`, `Unification.conv_current`, `Unification.conv_full`
  (`#20649 <https://github.com/rocq-prover/rocq/pull/20649>`_,
  fixes `#20579 <https://github.com/rocq-prover/rocq/issues/20579>`_,
  by Thomas Lamiaux).
- **Added:**
  antiquotation `$hyp:id` in terms for dynamically named hypotheses,
  i.e. `let x := @y in constr:($hyp:x)` is equivalent to `constr:(&y)`
  (`#20656 <https://github.com/rocq-prover/rocq/pull/20656>`_,
  by Gaëtan Gilbert).

.. _91ltac2notationfix:

- **Fixed:**
  Ltac2 in terms in notations is more aware of the notation variables it uses,
  providing early failure when the variable is instantiated with an invalid term,
  preventing a spurious warning when a variable that cannot be instantiated is unused,
  and preventing exponential blowups from copying unused data
  (`#20313 <https://github.com/coq/coq/pull/20313>`_,
  fixes `#17833 <https://github.com/coq/coq/issues/17833>`_
  and `#20188 <https://github.com/coq/coq/issues/20188>`_
  and `#20305 <https://github.com/coq/coq/issues/20305>`_,
  by Gaëtan Gilbert).

SSReflect
^^^^^^^^^

- **Changed:**
  `%FUN` now delimits scope `function_scope` rather than `fun_scope`
  in `ssrfun.v`
  (`#20478 <https://github.com/rocq-prover/rocq/pull/20478>`_,
  by Pierre Roux).
- **Removed:**
  scope `fun_scope` from `ssrfun.v` that was deprecated since 8.20,
  use `function_scope` instead
  (`#20478 <https://github.com/rocq-prover/rocq/pull/20478>`_,
  by Pierre Roux).
- **Deprecated:**
  `idempotent` in `ssrfun.v`, use `idempotent_op` instead
  (`#20478 <https://github.com/rocq-prover/rocq/pull/20478>`_,
  by Pierre Roux).
- **Added:**
  definitions `injective2`, `idempotent_op` and `idempotent_fun` and
  lemmas `omap_id`, `eq_omap`, `inj_omap`, `omapK`, `inr_inj` and
  `inl_inj` in `ssrfun.v`
  (`#20478 <https://github.com/rocq-prover/rocq/pull/20478>`_,
  by Pierre Roux).

Commands and options
^^^^^^^^^^^^^^^^^^^^

- **Changed:**
  commands taking a tactic argument (e.g. :cmd:`Hint Extern`)
  now follow :opt:`Default Proof Mode` instead of hardcoding Ltac1
  (`#19690 <https://github.com/coq/coq/pull/19690>`_,
  fixes `#13784 <https://github.com/coq/coq/issues/13784>`_,
  by Gaëtan Gilbert).
- **Changed:**
  :opt:`Printing Depth` completely skips subterms beyond the given depth.
  In general the formatter depth is higher than the term depth, so there is no visible change,
  but some notations print subterms without increasing the formatting depth in which case
  you may need to increase the printing depth to avoid `...`
  (`#20275 <https://github.com/coq/coq/pull/20275>`_,
  by Gaëtan Gilbert).
- **Changed:**
  :cmd:`Search` ignores lemmas declared with :attr:`local` unless
  new flag :flag:`Search Blacklist Locals` is unset
  (`#20349 <https://github.com/coq/coq/pull/20349>`_,
  by Gaëtan Gilbert).
- **Changed:**
  :cmd:`Search` now accepts open modules, including the current file with
  the  `in`, `inside` and `outside` filters.
  (`#20733 <https://github.com/coq/coq/pull/20733>`_,
  fixes `#14010 <https://github.com/coq/coq/issues/14010>`_,
  by Pierre Rousselin, with a lot of help by Gaëtan Gilbert).
- **Removed:**
  flag `Lia Enum`, which did nothing
  (`#20640 <https://github.com/rocq-prover/rocq/pull/20640>`_,
  by Gaëtan Gilbert).
- **Added:**
  :cmd:`Sort` to declare global or section-scoped sort qualities
  (`#18615 <https://github.com/coq/coq/pull/18615>`_,
  by Kenji Maillard).
- **Added:**
  :cmd:`Number Notation` and :cmd:`String Notation` understand parsers which may produce error messages
  (`#20107 <https://github.com/coq/coq/pull/20107>`_,
  fixes `#20042 <https://github.com/coq/coq/issues/20042>`_,
  by Gaëtan Gilbert).

.. _91refinedef:

- **Added:**
  support for the :attr:`refine` attribute to definitions and (co)fixpoints
  (`#20355 <https://github.com/coq/coq/pull/20355>`_,
  fixes `#20302 <https://github.com/coq/coq/issues/20302>`_,
  by Yann Leray).

Command-line tools
^^^^^^^^^^^^^^^^^^

- **Changed:**
  `rocq timelog2html` now needs package `rocq-devtools` to be installed
  (`#20169 <https://github.com/coq/coq/pull/20169>`_,
  by Gaëtan Gilbert).
- **Added:**
  error on ambiguous :cmd:`Require`. Rocq used to silently select a file
  when ambiguous :cmd:`Require`\s came from different loadpaths, for instance
  different fields of the ``ROCQPATH`` environment variable
  (`#20601 <https://github.com/rocq-prover/rocq/pull/20601>`_,
  fixes `#20587 <https://github.com/rocq-prover/rocq/issues/20587>`_,
  by Gaëtan Gilbert).
- **Fixed:**
  `rocq dep` implicitly adds `-I $rocq-runtime/..` after the explicit `-I` instead of before
  (where `$rocq-runtime` is the expected location of the rocq-runtime package).
  This means that if a local plugin (whose META is in an explicit `-I` path) is installed next to rocq-runtime,
  `rocq dep` will emit a dependency on the local version instead of the installed version
  (`#20393 <https://github.com/coq/coq/pull/20393>`_,
  by Gaëtan Gilbert).

RocqIDE
^^^^^^^

- **Changed:**
  default character encoding is UTF8 (it was locale dependent on non-windows OSes),
  and when the configured encoding is not UTF8 RocqIDE will attempt to convert input files even if they are already valid UTF8
  (`#20256 <https://github.com/coq/coq/pull/20256>`_,
  fixes `#11526 <https://github.com/coq/coq/issues/11526>`_,
  by Gaëtan Gilbert).
- **Added:**
  an option to control the maximum length of the message view
  in RocqIDE
  (`#20597 <https://github.com/rocq-prover/rocq/pull/20597>`_,
  fixes `#20420 <https://github.com/rocq-prover/rocq/issues/20420>`_,
  by Pierre-Marie Pédrot).

Corelib
^^^^^^^

- **Added:**
  type `result` in `Corelib.Datatypes`, equivalent to `sum`
  but with a name fitting possibly-failing computations
  (`#20107 <https://github.com/coq/coq/pull/20107>`_,
  by Gaëtan Gilbert).

Infrastructure and dependencies
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

- **Changed:**
  minimum supported OCaml version is now 4.14.0 (instead of 4.09.0),
  and minimum supported OCamlfind version is now 1.9.1 (instead of 1.8.1)
  (`#20576 <https://github.com/rocq-prover/rocq/pull/20576>`_,
  by Gaëtan Gilbert).

.. _91relocatable:

- **Added:**
  Rocq can be compile-time configured to be relocatable,
  using `./configure -relocatable` instead of e.g. `./configure -prefix /some/path`.
  See :ref:`system_config` for an explanation of how Rocq uses its configured installation paths
  (`#19901 <https://github.com/coq/coq/pull/19901>`_,
  by Gaëtan Gilbert).
- **Added:** Experimental support for native Windows builds.
  Rocq can now build and run under a native Windows environment using
  the new native Windows support in Opam 2.3. This setup is tested in
  CI, running a large part of the test suite. Beware this support is
  still experimental, and some problem may arise on Unix-specific
  tools. Note that RocqIDE is still not supported (c.f. `#20631
  <https://github.com/rocq-prover/rocq/issues/20631>`_) (`#20464
  <https://github.com/rocq-prover/rocq/pull/20464>`_, by Emilio Jesus
  Gallego Arias, Gaëtan Gilbert, David Allsopp, Ali Caglayan, Jason
  Gross, the Opam team, the @setup-ocaml team, the OCaml team).
- **Fixed:**
  Bad interaction between dune, `rocq dep`, and local opam directory switches
  (`#20437 <https://github.com/rocq-prover/rocq/pull/20437>`_,
  fixes `#20422 <https://github.com/rocq-prover/rocq/issues/20422>`_,
  by Rodolphe Lepigre).

Extraction
^^^^^^^^^^

.. _91extractsortpoly:

- **Fixed:**
  extraction handles sort polymorphic definitions
  (`#20655 <https://github.com/rocq-prover/rocq/pull/20655>`_,
  by Pierre-Marie Pédrot).

Miscellaneous
^^^^^^^^^^^^^

- **Added:**
  plugin tutorial for extending Ltac2
  (`#20670 <https://github.com/rocq-prover/rocq/pull/20670>`_,
  by Gaëtan Gilbert).

Version 9.0
-----------

.. contents::
   :local:
   :depth: 1

Summary of changes
~~~~~~~~~~~~~~~~~~

The Rocq Prover version 9.0 is the first Rocq Prover release after the renaming
from The Coq Proof Assistant. The Rocq Prover 9.0 command line interface is
backwards compatible with Coq 8.20, providing compatibility shims so that
developments depending on Coq can be easily ported, see `Porting to The Rocq
Prover`_  for details. The 9.0 version is based on a new single binary `rocq`
that dispatches commands to previously separate binaries, a split and renaming
of the standard library to `Stdlib` and improvements to the handling of
template-polymorphism, bringing it closer to a complete subsumption by sort
polymorphism.

We highlight some of the most impactful changes here:

  - "The Rocq Prover" is the new official name of the project. We leave to users the
    choice of renaming their projects to reflect this change, see `Renaming Advice`_.
    The Rocq Prover comes with a new visual identity and website, see `The Rocq Prover Website`_.

  - A single `rocq` binary dispatches commands for compilation, read-eval-print-loop,
    documentation building, dependency computation, etc. See :ref:`therocqcommands`.
    It corresponds to the `rocq-runtime` `opam package <https://ocaml.org/p/rocq-runtime>`_.
    This is a bare-bones package that does not provide any Gallina code.

  - The `Coq` standard library has been :ref:`split <90stdlib>` into two libraries:

    - A `Corelib` library (the `rocq-core` opam package). This is an
      extended prelude, which is
      enough to run Rocq tactics and contains the `Ltac2` library and bindings
      for primitive types (integers, floats, arrays and strings).
    - An `Stdlib` library (the `rocq-stdlib` opam package). The `Stdlib` is
      now maintained out of the main `rocq` repository. We welcome maintainers and
      contributors to the `new repository <https://github.com/rocq-prover/stdlib>`_.
      A specific call for contributions will be
      sent soon.

Notable breaking changes:

  - The legacy loading mode for plugins has been :ref:`removed <LegacyLoadingRemoval>`.

See the `Changes in 9.0.0`_ section below for the detailed list of changes,
including potentially breaking changes marked with **Changed**.
Rocq's `reference manual for 9.0 <https://rocq-prover.org/doc/v9.0/refman>`_,
documentation of the 9.0 `core <https://rocq-prover.org/doc/v9.0/corelib>`_ and
`standard <https://rocq-prover.org/doc/v9.0/stdlib>`_ libraries,
`reference manual of the 9.0 standard library <https://rocq-prover.org/doc/v9.0/refman-stdlib>`_
and `developer documentation of the 9.0 ML API <https://rocq-prover.org/doc/v9.0/api>`_
are also available.

Théo Zimmermann, with help from Jason Gross and Gaëtan Gilbert, 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>`_.

Ali Caglayan, Emilio Jesús Gallego Arias, Rudi Grinberg and Rodolphe Lepigre maintained the
`Dune build system for OCaml and Coq/Rocq <https://github.com/ocaml/dune/>`_
used to build the Rocq Prover itself and many Rocq projects.

The `opam repository <https://github.com/coq/opam>`_ for Rocq packages has been maintained by
Guillaume Claret, Guillaume Melquiond, Karl Palmskog, Matthieu Sozeau
and Enrico Tassi with contributions from many users. The up-to-date list
of packages is `available on the Rocq website <https://rocq-prover.org/packages>`_.

Erik Martin-Dorel and Jaime Arias maintained the
`Rocq Docker images <https://hub.docker.com/r/rocq/rocq-prover>`_.
Erik Martin-Dorel maintained the `docker-keeper <https://gitlab.com/erikmd/docker-keeper>`_ compiler
used to build and keep those images up to date (note that the tool is not Rocq specific).
Erik Martin-Dorel and Théo Zimmermann maintained the
`docker-coq-action <https://github.com/coq-community/docker-coq-action>`_
container action (which is applicable to any opam project hosted on GitHub).

Cyril Cohen, Vincent Laporte, Pierre Roux and Théo Zimmermann
maintained the `Nix toolbox <https://github.com/coq-community/coq-nix-toolbox>`_.
The docker-coq-action and the Nix toolbox are used by many Rocq projects for continuous integration.

Rocq 9.0 was made possible thanks to the following 27 reviewers:
Yves Bertot, Ali Caglayan, Tej Chajed, Andres Erbsen, Jim Fehrle,
Emilio Jesús Gallego Arias, Gaëtan Gilbert, Jason Gross, Samuel Gruetter,
Hugo Herbelin, Thomas Lamiaux, Olivier Laurent, Rodolphe Lepigre,
Erik Martin-Dorel, Guillaume Melquiond, Guillaume Munch-Maccagnoni,
Karl Palmskog, Pierre-Marie Pédrot, Pierre Rousselin, Pierre Roux,
Marcello Seri, Michael Soegtrop, Matthieu Sozeau, Enrico Tassi,
Romain Tetley, Oliver Turner and Théo Zimmermann.

See the `Rocq Team <https://rocq-prover.org/rocq-team>`_ page for
more details on Rocq's development teams.

The 48 contributors to the 9.0 version are:
Jean Abou Samra, Tanaka Akira, David Allsopp, Frédéric Besson, Mathis Bouverot, Sylvain Chiron,
Cyril Cohen, Lucas Donati, Andrej Dudenhefner, Arya Elfren, Andres Erbsen, Siegmentation Fault,
Jim Fehrle, Gaëtan Gilbert, Tomaz Gomes Mascarenhas, Jason Gross, Hugo Herbelin, Florent Hivert,
Daniil Iaitskov, Emilio Jesús Gallego Arias, Jan-Oliver Kaiser, Rodolphe Lepigre, Yann Leray,
Felix Loyau-Kahn, Erik Martin-Dorel, Guillaume Melquiond, Guillaume Munch-Maccagnoni,
Aleksandar Nanevski, Charles Norton, Karl Palmskog, Pierre-Marie Pédrot, Pierre Rousselin,
Pierre Roux, Kazuhiko Sakaguchi, Gabriel Scherer, Marcello Seri, Benny Smit, Michael Soegtrop,
Matthieu Sozeau, Nicolas Tabareau, Enrico Tassi, Oliver Turner, Quentin Vermande, Daneel Yaitskov,
Remzi Yang, Tan Yee Jian and Théo Zimmermann.

The Coq/Rocq community at large helped improve this new version via
the GitHub issue and pull request system, the coq-club@inria.fr mailing list,
the `Discourse forum <https://coq.discourse.group/>`_ and the
`Coq Zulip chat <https://coq.zulipchat.com>`_.

Version 9.0's development spanned 7 months from the release of Coq 8.20.0.
Pierre-Marie Pédrot and Matthieu Sozeau are the release managers of Rocq 9.0.
This release is the result of 491 merged PRs, closing 68 issues.

| Nantes, March 2025
| Pierre-Marie Pédrot and Matthieu Sozeau for the Rocq development team

Porting to The Rocq Prover
~~~~~~~~~~~~~~~~~~~~~~~~~~

The Rocq Prover version 9.0 includes compatibility shims that make it possible
to invoke it through legacy Coq commands: `coq-tex`, `coq_makefile`, `coqchk`, `coqdoc`, `coqpp`, `coqtop`,
`coqwc`, `coqc`, `coqdep`, `coqnative`, `coqtimelog2html`, `coqtop.byte`, `coqworkmgr`.
When using `opam`, this compatibility layer is provided by the packages `coq-core`,
`coq-stdlib` and `coq`. In this setting, nothing needs to be changed to the build systems
of existing projects to compile with Rocq 9.0 (aliased as "Coq 9.0").

You should expect warnings that the standard library previously under namespace
`Coq` has been renamed to `Stdlib`. See `this entry
<https://rocq-prover.org/doc/v9.0/refman-stdlib/changes.html#changed>`_ from
the Standard Library's changelog for the suggested workflow to port theories.

There are important changes to consider for building plugins and libraries:

- To be future-proof, projects based on `coq_makefile` can be ported to not rely
  on the compatibility layer anymore. To do so, one must replace uses of
  `coq_makefile` with :ref:`rocq makefile <rocq_makefile>`, which will directly
  call the new `rocq` binary without relying on the compatibility shims.

- If using `dune` to :ref:`build <building_dune>` a Rocq project, you will still
  need the compatibility shim for `coq-core` so that `dune`'s Coq language extension
  functions correctly.

Regarding packaging:

- Opam packages that depend on the compatibility shims should remain named as `coq-*`, whereas
  ported packages should be named `rocq-*`, with the `coq` dependency being replaced by
  a `rocq-core` and `rocq-stdlib` dependency (unless your package does not depend on the stdlib),
  but **not** `rocq-prover` which is only a user-oriented metapackage.
- Similarly, Nix packages that use the compatibility shims can be kept in
  `coqPackages` (and can keep depending on `coq`), whereas ported packages can
  be added in `rocqPackages`, depending on `rocq-core`.

In both cases, when a `rocq` port is done, a `coq` metapackage can be kept,
simply depending on the new `rocq` package and `coq`.

Renaming Advice
~~~~~~~~~~~~~~~

We have applied the `renaming <https://rocq-prover.org/about#Name>`_ from the
Coq Proof Assistant to The Rocq Prover in this version, and officialy supported
projects in the `Rocq organization <https://github.com/rocq-prover>`_ will be
renamed in the future. The Rocq Development Team's official position on renaming of
projects *it does not officially maintain* is to let their authors do as they wish.
We just note that the new identity is quite compatible with existing
Rooster references. However, we encourage existing and forthcoming projects to
adopt the new logo, its colors and fonts, see the `identity guidelines
<https://rocq-prover.org/logo>`_ for more information.

The Rocq Prover Website
~~~~~~~~~~~~~~~~~~~~~~~

The Rocq Prover comes with a new `website <https://rocq-prover.org>`_ which was
developped by Matthieu Sozeau, Nicolas Tabareau and Théo Zimmermann in
collaboration with Bastien Sozeau of the `Noir Blanc Rouge
<https://noirblancrouge.com/>`_ type foundry. The new website is a fork of the
`OCaml.org <https://ocaml.org>`_ website developed by `Tarides
<https://tarides.com/>`_. The Rocq development team is thankful for their help
and for open-sourcing their website. It includes full support for the `Rocq
package archive <https://github.com/coq/opam>`_, a responsive design and easy
contributions through markdown files. The new identity, customized fonts and
logo were designed by Bastien Sozeau, consulting for the Rocq development team.
The logo is released under the UNLICENSE open-source `license <https://github.com/coq/rocq-prover.org/LICENSE>`_
and customized 3rd-party fonts are released under open-source `licences <https://github.com/coq/rocq-prover.org/LICENSE-3RD-PARTY>`_.

The website is deployed automatically using a
custom `deployer <https://deploy.rocq-prover.org>`_ developed by Matthieu
Sozeau. The deployer keeps the website up-to-date with the GitHub repositories
of the `website <https://github.com/coq/rocq-prover.org>`__ and `documentation
<https://github.com/coq/doc>`_. Its code is accessible on `GitHub
<https://github.com/coq/deploy-rocq-prover.org>`_.

Changes in 9.0.0
~~~~~~~~~~~~~~~~

.. contents::
   :local:

Kernel
^^^^^^

- **Changed:**
  large performance improvements in kernel checking of terms with repeated subterms
  (`#19160 <https://github.com/coq/coq/pull/19160>`_,
  by Gaëtan Gilbert)
- **Changed:**
  the criteria for a parameter to be considered template in a template inductive type.
  For a level to be template, it must now appear only once in the context of parameters,
  and only as the return sort of the arity of some parameter. Furthermore,
  it may appear neither in the indices of the inductive type nor in the type of its constructors.
  Finally, a template level appearing in the return sort of the inductive type must have a zero increment
  (`#19250 <https://github.com/coq/coq/pull/19250>`_,
  `#19254 <https://github.com/coq/coq/pull/19254>`_,
  `#19263 <https://github.com/coq/coq/pull/19263>`_,
  by Pierre-Marie Pédrot).
- **Changed:**
  the kernel typing rules for template polymorphic inductive types do not
  require anymore adding global constraints when applied enough. Rather,
  template polymorphic inductive types are now a special kind of universe
  polymorphic inductive types that do not need explicit instances and
  can handle some amount of algebraic universe levels. The new rules are
  strictly more general than the previous ones and thus backwards compatible
  (`#19262 <https://github.com/coq/coq/pull/19262>`_,
  by Pierre-Marie Pédrot).
- **Removed:**
  the kernel always produces an error when given terms with bad relevances
  instead of emitting the default-error `bad-relevance` warning
  (which is now only used by the higher layers)
  (`#19164 <https://github.com/coq/coq/pull/19164>`_,
  by Gaëtan Gilbert).

Specification language, type inference
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

- **Changed:**
  Typeclasses queries of classes that are declared with the options
  `Typeclasses Strict Resolution` and `Typeclasses Unique Instances`
  enabled are resolved independently of other queries, allowing them
  to succeed even when the remaining queries fail
  (`#18762 <https://github.com/coq/coq/pull/18762>`_,
  by Jan-Oliver Kaiser).
- **Changed:**
  More systematic early check of `@{univs}`-like universe declarations
  at the time of declaring the statement of an interactive
  definition/theorem
  (`#18960 <https://github.com/coq/coq/pull/18960>`_,
  by Hugo Herbelin).
- **Changed:**
  The syntax :n:`Derive x SuchThat type As name` is deprecated and replaced by
  :n:`Derive x in type as name` which itself is generalized into
  :n:`Derive open_binders in type as name`, so that several names,
  and possibly types to these names, can be given
  (`#19295 <https://github.com/coq/coq/pull/19295>`_,
  by Hugo Herbelin).
- **Changed:**
  `match` elaboration can unify sort quality variables to make an elimination valid
  (`#19329 <https://github.com/coq/coq/pull/19329>`_,
  fixes `#19327 <https://github.com/coq/coq/issues/19327>`_,
  by Gaëtan Gilbert).
- **Changed:**
  ``:>`` in :token:`of_type_inst` now always declares coercions. The previous behavior,
  deprecated since 8.18, was to declare typeclass instances instead,
  when used in records declared with the :cmd:`Class` keyword. Look at
  the :ref:`previous changelog entries <819_changes_spec_language>`
  about former warnings `future-coercion-class-constructor` and
  `future-coercion-class-field` for advice on how to update your code
  (`#19519 <https://github.com/coq/coq/pull/19519>`_, by Pierre Roux).
- **Changed:**
  The unification algorithm does not solve unification problems of the
  form `proj _ ~ _` using canonical structures when the LHS reduces or
  is ground
  (`#19611 <https://github.com/coq/coq/pull/19611>`_,
  by Quentin Vermande).
- **Changed:**
  When unification fails to instantiate an evar because
  of a problem that occurs under a beta-redex, we reduce
  this beta-redex and try again
  (`#19833 <https://github.com/coq/coq/pull/19833>`_,
  by Quentin Vermande).
- **Added:**
  Ability to hide the quantification over the decreasing argument of a
  fixpoint under a definition, with application to declaring fixpoints
  as instance of a class
  (`#19296 <https://github.com/coq/coq/pull/19296>`_,
  fixes `#7913 <https://github.com/coq/coq/issues/7913>`_,
  by Hugo Herbelin).
- **Fixed:**
  :cmd:`Derive` now supports :cmd:`Admitted`
  (`#19092 <https://github.com/coq/coq/pull/19092>`_,
  fixes `#18951 <https://github.com/coq/coq/issues/18951>`_,
  by Hugo Herbelin).
- **Fixed:**
  Mishandling of let binders in `Program Fixpoint`
  (`#19257 <https://github.com/coq/coq/pull/19257>`_,
  fixes `#16906 <https://github.com/coq/coq/issues/16906>`_,
  by Hugo Herbelin).
- **Fixed:**
  Pattern-matching in :attr:`Program` mode now supports inductive
  types using :ref:`local definitions <let-in>` in their declaration
  (`#19773 <https://github.com/coq/coq/pull/19773>`_,
  fixes `#10407 <https://github.com/coq/coq/issues/10407>`_,
  by Hugo Herbelin).
- **Fixed:**
  Anomaly in :cmd:`Function` when a well-founded relation had not the expected type
  (`#19775 <https://github.com/coq/coq/pull/19775>`_,
  fixes `#12417 <https://github.com/coq/coq/issues/12417>`_,
  by Hugo Herbelin).

Notations
^^^^^^^^^

- **Fixed:**
  Recognized all Unicode non-spacing marks as valid identifier characters
  (`#19693 <https://github.com/coq/coq/pull/19693>`_,
  fixes `#19512 <https://github.com/coq/coq/issues/19512>`_,
  by Guillaume Melquiond).

Tactics
^^^^^^^

- **Changed:**
  The reduction tactic :tacn:`hnf` becomes insensitive to the
  :g:`simpl never` status of constants, as prescribed in the reference
  manual; this can exceptionally impact the behavior of :tacn:`intros`
  on goals defining an implicative or universally quantified statement
  by recursion (`#18580 <https://github.com/coq/coq/pull/18580>`_,
  by Hugo Herbelin).
- **Changed:**
  `Ncring_tac.extra_reify` is expected to return `tt` on failure and
  the reification result on success, instead of `(false, anything)` on failure
  and `(true, result)` on success
  (this only matters to users overriding it to extend the Ncring reification)
  (`#19501 <https://github.com/coq/coq/pull/19501>`_,
  by Gaëtan Gilbert).
- **Removed:**
  the deprecated `gintuition` tactic
  (`#19704 <https://github.com/coq/coq/pull/19704>`_,
  by Pierre-Marie Pédrot).
- **Removed:**
  `dfs eauto` tactic, which was deprecated in 8.16
  (`#19817 <https://github.com/coq/coq/pull/19817>`_,
  by Jim Fehrle).
- **Added:**
  The :flag:`Info Micromega` flag (unset by default) makes :tacn:`lia`,
  :tacn:`lra`, :tacn:`nia` and :tacn:`nra` print the names of
  hypotheses used by the proof
  (`#19703 <https://github.com/coq/coq/pull/19703>`_,
  by Frédéric Besson).
- **Fixed:**
  Refolding of constants marked as :g:`simpl never` in position of
  argument of a destructor in :tacn:`simpl`; note that this may
  occasionally cause some calls to :tacn:`simpl` to satisfy more
  scrupulously :g:`simpl never` and to stop reducing further in
  subterms that are *not* in position of argument of a destructor, as
  specified by :g:`simpl never`
  (`#18591 <https://github.com/coq/coq/pull/18591>`_,
  fixes `#16040 <https://github.com/coq/coq/issues/16040>`_,
  by Hugo Herbelin).
- **Fixed:**
  `Set Typeclasses Strict Resolution` is no longer ignored in
  `typeclasses eauto with <dbs>`
  (`#19436 <https://github.com/coq/coq/pull/19436>`_,
  fixes `#15432 <https://github.com/coq/coq/issues/15432>`_,
  by Jan-Oliver Kaiser).
- **Fixed:**
  Unbound variables were sometimes generated when a metavariable of a
  theorem given to :tacn:`apply` occurred in the type of the theorem
  under a :n:`fun`
  (`#19769 <https://github.com/coq/coq/pull/19769>`_,
  fixes `#17314 <https://github.com/coq/coq/issues/17314>`_,
  by Hugo Herbelin).
- **Fixed:**
  `cbn` now considers primitive literals (integers, floats, arrays, strings)
  "constructors", i.e. they now satisfy the `!` modifier in `Arguments`
  (`#20004 <https://github.com/coq/coq/pull/20004>`_,
  fixes `#20003 <https://github.com/coq/coq/issues/20003>`_,
  by Jan-Oliver Kaiser).

Ltac2 language
^^^^^^^^^^^^^^

- **Deprecated:**
  `Ltac2.Constr.occur_between` and `occurn` whose return values are the opposite of that implied by their names
  (`#19614 <https://github.com/coq/coq/pull/19614>`_,
  by Gaëtan Gilbert).
- **Added:**
  Added Ltac2 bindings for congruence and simpl congruence, it fixes #14289 not entirely but provides Ltac2 bindings for one of the tactics listed there
  (`#19032 <https://github.com/coq/coq/pull/19032>`_,
  fixes `#14289 <https://github.com/coq/coq/issues/14289>`_,
  by Benny Smit, reviewed by Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert).
- **Added:**
  APIs `compare` `of_int` and `print` in `Ltac2.Uint63`
  (`#19197 <https://github.com/coq/coq/pull/19197>`_,
  by Gaëtan Gilbert).
- **Added:**
  :cmd:`Ltac2 Type` supports deprecation of the declared constructors
  (`#19575 <https://github.com/coq/coq/pull/19575>`_,
  by Gaëtan Gilbert).
- **Added:**
  `Ltac2.Constr.noccur_between` and `noccurn` to test for non-occurrence of local variables in terms
  (`#19614 <https://github.com/coq/coq/pull/19614>`_,
  by Gaëtan Gilbert).
- **Added:**
  `Ltac2.Control.hyp_value` to get the value (`v` in `H := v`) of an hypothesis
  (`#19630 <https://github.com/coq/coq/pull/19630>`_,
  by Gaëtan Gilbert).
- **Fixed:**
  resolution of :ref:`abbreviations <Abbreviations>` in :n:`reference`
  in :token:`ltac2_quotations`, for instance in eval tactic
  delta-reduction flags :token:`ltac2_delta_reductions`
  (`#19589 <https://github.com/coq/coq/pull/19589>`_,
  fixes `#19590 <https://github.com/coq/coq/issues/19590>`_,
  by Pierre Roux).
- **Fixed:**
  `Ltac2 Eval` does not require to be focused in a goal
  anymore (`#19961 <https://github.com/coq/coq/pull/19961>`_, by
  Daniil Iaitskov).

SSReflect
^^^^^^^^^

- **Changed:**
  The :tacn:`done` tactic now tries to apply `sym_equal` with four arguments
  instead of trying first with zero to three arguments
  (`#19372 <https://github.com/coq/coq/pull/19372>`_,
  by Quentin Vermande).
- **Changed:**
  `done` uses `simple refine` instead of `apply` to apply `sym_equal`
  (`#19399 <https://github.com/coq/coq/pull/19399>`_,
  by Quentin Vermande).
- **Removed:**
  no longer used lemma ``not_locked_false_eq_true``
  and its call in the :tacn:`done` tactic
  (`#19382 <https://github.com/coq/coq/pull/19382>`_,
  by Pierre Roux).

Commands and options
^^^^^^^^^^^^^^^^^^^^

- **Changed:**
  :cmd:`Variables` and its aliases do not share the type of combined binders anymore.
  This makes for instance `Variables a b : T` strictly equivalent to `Variables (a: T) (b : T).`
  (when `a` is not bound in `T`).
  The difference matters when interpreting `T` generates fresh universes or existential variables:
  they will be distinct in the types of `a` and `b`.
  This was already the case for binders in terms (eg `fun (a b : T) => ...`), :cmd:`Context`,
  and when :flag:`Universe Polymorphism` is enabled
  (`#19277 <https://github.com/coq/coq/pull/19277>`_,
  by Gaëtan Gilbert).
- **Changed:**
  :cmd:`Guarded` and :cmd:`Validate Proof` are now internally classified as "queries" instead of "proof steps".
  This means they should not be counted anymore when stepping back with :cmd:`Undo`.
  (`#19383 <https://github.com/coq/coq/pull/19383>`_,
  by Gaëtan Gilbert).
- **Changed:**
  template polymorphism can bind universes which do not appear in the inductive's conclusion.
  For instance `eq` and `ex` are now template polymorphic.
  (`#19528 <https://github.com/coq/coq/pull/19528>`_,
  by Gaëtan Gilbert).
- **Changed:**
  The order of hints shown in the "For any goal" category in :cmd:`Print HintDb`
  now matches the order in which they will be tried.
  Previously the entries were misordered on their priority
  (`#19624 <https://github.com/coq/coq/pull/19624>`_,
  by Jim Fehrle).
- **Changed:**
  The :cmd:`Hint Rewrite` command now requires a *non-empty* list of hintDbs
  after the colon to be consistent with other Hint commands.  If your script
  has an empty list of hintDbs, fix it by removing the colon
  (`#19730 <https://github.com/coq/coq/pull/19730>`_,
  by Jim Fehrle).
- **Changed:**
  :cmd:`Create HintDb` no longer erases pre-existing hint databases
  (`#19808 <https://github.com/coq/coq/pull/19808>`_,
  by Gaëtan Gilbert).

.. _LegacyLoadingRemoval:

- **Removed:**
  "legacy" (non-findlib) loading mode for plugins in :cmd:`Declare ML Module`
  (`#18385 <https://github.com/coq/coq/pull/18385>`_,
  by Emilio Jesús Gallego Arias and Gaëtan Gilbert).
- **Removed:**
  :n:`: @type` annotation in :cmd:`Obligation` which was ignored when executing the command
  (`#19678 <https://github.com/coq/coq/pull/19678>`_,
  by Gaëtan Gilbert).
- **Removed:**
  flag `Automatic Proposition Inductives` (using its effect was deprecated since 8.20)
  (`#19872 <https://github.com/coq/coq/pull/19872>`_,
  by Gaëtan Gilbert).
- **Added:**
  New :cmd:`Arguments`' modifier `clear simpl` to reset `simpl` reduction flags
  (`#19216 <https://github.com/coq/coq/pull/19216>`_,
  by Hugo Herbelin).
- **Added:**
  The ``use`` field of the :attr:`deprecated` attribute lets one specify
  a replacement for a ``Theorem``, ``Definition`` or ``Notation`` that is
  printed as part of the deprecation warning message and also used to suggest
  a quick fix in LSP based user interfaces
  (`#19300 <https://github.com/coq/coq/pull/19300>`_,
  by Enrico Tassi).
- **Added:**
  :cmd:`Register`, :cmd:`Register Scheme` and :cmd:`Add Zify`
  now support attributes :attr:`local`, :attr:`export` and :attr:`global`
  (`#19362 <https://github.com/coq/coq/pull/19362>`_,
  by Gaëtan Gilbert).
- **Added:**
  :cmd:`Add` and :cmd:`Remove`
  now support attributes :attr:`local`, :attr:`export` and :attr:`global`
  (`#19390 <https://github.com/coq/coq/pull/19390>`_,
  by Gaëtan Gilbert).
- **Added:**
  Default hint mode option for typeclasses, mode attribute on Class
  declarations overriding the default and class-declaration-default-mode
  warning to check for uses of the default mode
  (`#19473 <https://github.com/coq/coq/pull/19473>`_,
  by Matthieu Sozeau).
- **Added:**
  :cmd:`Profile` command modifier to get profiling information for a given command
  (`#19517 <https://github.com/coq/coq/pull/19517>`_,
  by Gaëtan Gilbert).
- **Added:**
  :cmd:`Print Universes` `Subgraph` accepts raw universe names (which end in an integer instead of an identifier)
  for debugging purposes, eg `Print Universes Subgraph ("foo.1" "foo.2")`.
  The integer in raw universe expressions is extremely unstable,
  so raw universe expressions should not be used outside debugging sessions
  (`#19640 <https://github.com/coq/coq/pull/19640>`_,
  by Gaëtan Gilbert).
- **Fixed:**
  the effect of :cmd:`Export` survives sections
  (the previous behaviour was identical to :cmd:`Import` in sections)
  (`#19361 <https://github.com/coq/coq/pull/19361>`_,
  fixes `#19360 <https://github.com/coq/coq/issues/19360>`_,
  by Gaëtan Gilbert).
- **Fixed:**
  Anomaly when printing a module functor with :cmd:`Strategy` or
  :cmd:`Transparent` in one of its parameters
  (`#19768 <https://github.com/coq/coq/pull/19768>`_,
  fixes `#19767 <https://github.com/coq/coq/issues/19767>`_,
  by Hugo Herbelin).
- **Fixed:**
  :opt:`Debug` and :opt:`Warnings` are classified as Synterp.
  This changes the scheduling during :cmd:`Import` such that putting `#[export] Set Warnings` around a specific command may change behaviour.
  (`#19981 <https://github.com/coq/coq/pull/19981>`_,
  by Gaëtan Gilbert).

Command-line tools
^^^^^^^^^^^^^^^^^^

- **Changed:**
  The ``-compat`` :ref:`command line option <command-line-options>`
  now raises a warning rather than an error when the compatibility file
  doesn't exist. This enables easier use of the compat mechanism with
  versions where the compatibility file doesn't exist yet
  (`#19370 <https://github.com/coq/coq/pull/19370>`_,
  by Pierre Roux).
- **Changed:**
  `coq_makefile` generated makefiles only install plugin `.cmxs` files in findlib locations
  and stop putting a copy in `user-contrib` (the copy should be useless after the removal of plugin legacy loading)
  (`#19841 <https://github.com/coq/coq/pull/19841>`_,
  by Gaëtan Gilbert).
- **Removed:**
  `coqdep` flag `-m` (it was used through `coq_makefile`)
  (`#19863 <https://github.com/coq/coq/pull/19863>`_,
  by Gaëtan Gilbert).
- **Added:**
  :ref:`command line option <command-line-options>` ``-compat-from``
  to enable writing compatibility files for libraries similarly to the
  ``-compat`` option for Rocq
  (`#19370 <https://github.com/coq/coq/pull/19370>`_,
  by Pierre Roux).
- **Added:**
  The ``-compat`` :ref:`command line option <command-line-options>`
  now silences deprecation warnings that were introduced since the
  given version
  (`#19370 <https://github.com/coq/coq/pull/19370>`_,
  by Pierre Roux).

RocqIDE
^^^^^^^

- **Changed:**
  Improved Preferences dialog: larger margins,
  tree of categories, sections in the categories,
  spin buttons for numbers, preservation of the last
  selected category, and more
  (`#19417 <https://github.com/coq/coq/pull/19417>`_,
  by Sylvain Chiron).
- **Fixed:**
  All preferences are now applied after clicking Apply or OK
  rather than immediately
  (`#19417 <https://github.com/coq/coq/pull/19417>`_,
  by Sylvain Chiron).
- **Fixed:**
  Changing the allowed modifiers in the Shortcuts panel of
  the Preferences dialog now immediately updates the available
  modifiers for the listed items
  (`#19417 <https://github.com/coq/coq/pull/19417>`_,
  by Sylvain Chiron).
- **Added:**
  Preference setting for unjustified conclusions background color
  (`#19417 <https://github.com/coq/coq/pull/19417>`_,
  by Sylvain Chiron).
- **Changed:**
  CoqIDE is renamed to RocqIDE (the auxiliary binary `coqidetop` is not renamed)
  (`#20036 <https://github.com/coq/coq/pull/20036>`_,
  by Gaëtan Gilbert).
- **Added:**
  Warnings are now included in the Errors panel
  (`#19188 <https://github.com/coq/coq/pull/19188>`_,
  by Jim Fehrle).
- **Fixed:**
  Changing the position of buffer names (top, left,
  bottom or right) no longer needs a restart
  (`#19166 <https://github.com/coq/coq/pull/19166>`_,
  by Sylvain Chiron).
- **Added:**
  Document tabs are now reorderable
  (`#19166 <https://github.com/coq/coq/pull/19166>`_,
  by Sylvain Chiron).

Standard library
^^^^^^^^^^^^^^^^

.. _90stdlib:

- **Changed:**
  Stdlib moved to its own repository, look for
  `Stdlib own changelog <https://rocq-prover.org/doc/v9.0/refman-stdlib/changes.html>`_
  for other changes there
  (`#19975 <https://github.com/coq/coq/pull/19975>`_,
  by Pierre Roux).
- **Added:**
  a new `rocq-core` package for users who don't want to depend on Stdlib.
  This provides `Corelib <https://rocq-prover.org/doc/v9.0/corelib>`_ a tiny subset of Stdlib
  (`#19530 <https://github.com/coq/coq/pull/19530>`_,
  starting to implement `CEP#83 <https://github.com/coq/ceps/pull/83>`_
  by Pierre Roux).

Infrastructure and dependencies
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

- **Changed:**
  when building Coq, the makefile's `world` target and `dune build`'s default target do not build rocqide anymore.
  Use `make world rocqide` or `dune build @default rocqide.install` to build what they respectively used to build
  (`#19378 <https://github.com/coq/coq/pull/19378>`_,
  by Gaëtan Gilbert).
- **Changed:**
  `coq_makefile` generates profiling info for `coqc` in `foo.vo.prof.json.gz` instead of `foo.v.prof.json.gz`
  (`#19428 <https://github.com/coq/coq/pull/19428>`_,
  by Gaëtan Gilbert).
- **Added:**
  `coq_makefile` generates profiling info for `coqchk` in `validate.prof.json.gz`
  (`#19428 <https://github.com/coq/coq/pull/19428>`_,
  by Gaëtan Gilbert).
- **Changed:**
  minimal Dune version required to build Coq bumped to 3.8.3
  (`#19621 <https://github.com/coq/coq/pull/19621>`_,
  by Pierre Roux).

Miscellaneous
^^^^^^^^^^^^^

- **Changed:**
  the current working directory is not implicitly added to the ML search path
  (`#19834 <https://github.com/coq/coq/pull/19834>`_,
  by Gaëtan Gilbert).
- **Changed:**
  the `user-contrib`, XDG and `COQPATH` directories are not implicitly added to the ML loadpath
  (`#19842 <https://github.com/coq/coq/pull/19842>`_,
  by Gaëtan Gilbert).

Version 8.20
------------

Summary of changes
~~~~~~~~~~~~~~~~~~

Coq version 8.20 adds a new rewrite rule mechanism along with a few
new features, a host of improvements to the virtual machine, the
notation system, Ltac2 and the standard library.

We highlight some of the most impactful changes here:

  - :ref:`rewrite_rules`

  - `primitive strings <https://github.com/coq/coq/pull/18973>`_

  - A lot of work went into reducing the size of the bytecode segment,
    which in turn means that .vo files might now be considerably
    smaller.

  - A new version of the
    `docker-keeper <https://gitlab.com/erikmd/docker-keeper>`_ compiler to
    build and maintain Docker images of Coq.

Notable breaking changes:

  - Syntactic global references passed through the `using` clauses of
    :tacn:`auto`-like tactics are now handled as plain references
    rather than interpreted terms. In particular, their typeclass
    arguments will not be inferred. In general, the previous behaviour
    can be emulated by replacing `auto using foo` with `pose proof
    foo; auto`.

  - Argument order for the Ltac2 combinators `List.fold_left2` and
    `List.fold_right2` changed to be the same as in OCaml.

  - :cmd:`Import`\ing a module containing a mutable Ltac2 definition
    does not undo its mutations. Replace `Ltac2 mutable foo :=
    some_expr.` with `Ltac2 mutable foo := some_expr. Ltac2 Set foo :=
    some_expr.` to recover the previous behaviour.

  - Some :ref:`renaming <820_renaming_stdlib>` in the standard
    library. Deprecations are provided for a smooth transition.

See the `Changes in 8.20.0`_ section below for the detailed list of changes,
including potentially breaking changes marked with **Changed**.
Coq's `reference manual for 8.20 <https://coq.github.io/doc/v8.20/refman>`_,
`documentation of the 8.20 standard library <https://coq.github.io/doc/v8.20/stdlib>`_
and `developer documentation of the 8.20 ML API <https://coq.github.io/doc/v8.20/api>`_
are also available.

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>`_.

Erik Martin-Dorel maintained the
`Coq Docker images <https://hub.docker.com/r/coqorg/coq>`_
and the `docker-keeper <https://gitlab.com/erikmd/docker-keeper>`_ compiler
used to build and keep those images up to date (note that the tool is not Coq specific).
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>`_.

Coq 8.20 was made possible thanks to the following reviewers:
Frédéric Besson, Lasse Blaauwbroek, Ali Caglayan, Cyril Cohen, Andrej
Dudenhefner, Andres Erbsen, Jim Fehrle, Emilio Jesús Gallego Arias,
Gaëtan Gilbert, Jason Gross, Hugo Herbelin, Ralf Jung, Jan-Oliver
Kaiser, Chantal Keller, Olivier Laurent, Rodolphe Lepigre, Yishuai Li,
Ralph Matthes, Guillaume Melquiond, Pierre-Marie Pédrot, Karl
Palmskog, Clément Pit-Claudel, Pierre Rousselin, Pierre Roux, Michael
Soegtrop, soukouki, Matthieu Sozeau, Nicolas Tabareau, Enrico Tassi,
Niels van der Weide, Nickolai Zeldovich and Théo Zimmermann. See the
`Coq Team face book <https://coq.inria.fr/coq-team.html>`_ page for
more details on Coq's development team.

The 59 contributors to the 8.20 version are:
Timur Aminev, Frédéric Besson, Lasse Blaauwbroek, Björn Brandenburg,
Ali Caglayan, Nikolaos Chatzikonstantinou, Sylvain Chiron, chluebi,
Cyril Cohen, Anton Danilkin, Louise Dubois de Prisque, Andrej
Dudenhefner, Maxime Dénès, Andres Erbsen, Jim Fehrle, Davide Fissore,
Andreas Florath, Yannick Forster, Mario Frank, Gaëtan Gilbert, Georges
Gonthier, Jason Gross, Stefan Haan, Hugo Herbelin, Lennart Jablonka,
Emilio Jesús Gallego Arias, Ralf Jung, Jan-Oliver Kaiser, Evgenii
Kosogorov, Rodolphe Lepigre, Yann Leray, David M. Cooke, Erik
Martin-Dorel, Guillaume Melquiond, Guillaume Munch-Maccagnoni, Karl
Palmskog, Julien Puydt, Pierre-Marie Pédrot, Ramkumar Ramachandra,
Pierre Rousselin, Pierre Roux, Kazuhiko Sakaguchi, Bernhard Schommer,
Remy Seassau, Matthieu Sozeau, Enrico Tassi, Romain Tetley, Laurent
Théry, Alexey Trilis, Oliver Turner, Quentin Vermande, Li-yao Xia and
Théo Zimmermann,

The Coq community at large helped improve this new version via
the GitHub issue and pull request system, the coq-club@inria.fr mailing list,
the `Discourse forum <https://coq.discourse.group/>`_ and the
`Coq Zulip chat <https://coq.zulipchat.com>`_.

Version 8.20's development spanned 7 months from the release of Coq 8.19.0
(9 months since the branch for 8.19.0).
Pierre Roux and Guillaume Melquiond are the release managers of Coq 8.20.
This release is the result of 470 merged PRs, closing 113 issues.

| Toulouse, September 2024
| Pierre Roux and Guillaume Melquiond for the Coq development team

Changes in 8.20.0
~~~~~~~~~~~~~~~~~

.. contents::
   :local:

Kernel
^^^^^^

- **Changed:**
  The guard checker now recognizes uniform parameters of a
  fixpoint and treats their instances as constant over the recursive call
  (`#17986 <https://github.com/coq/coq/pull/17986>`_,
  grants `#16040 <https://github.com/coq/coq/issues/16040>`_,
  by Hugo Herbelin).
- **Added:**
  A mechanism to add user-defined rewrite rules to Coq's reduction mechanisms;
  see chapter :ref:`rewrite_rules`
  (`#18038 <https://github.com/coq/coq/pull/18038>`_,
  by Yann Leray).
- **Added:** Support for primitive strings in terms
  (`#18973 <https://github.com/coq/coq/pull/18973>`_,
  by Rodolphe Lepigre).

.. _819_changes_spec_language:

Specification language, type inference
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

- **Changed:**
  warnings `future-coercion-class-constructor`
  and `future-coercion-class-field` about ``:>`` in :cmd:`Class` as
  errors by default. This offers a last opportunity to replace ``:>``
  with ``::`` (available since Coq 8.18) to declare typeclass instances
  before making ``:>`` consistently declare coercions in all records in
  next version.
  To adapt huge codebases, you can try
  `this script <https://gist.github.com/JasonGross/59fc3c03664f2280849abf50b531be42>`_
  or the one below. But beware that both are incomplete.

  .. code-block:: sh

     #!/bin/awk -f
     BEGIN {
       startclass = 0;
       inclass = 0;
       indefclass = 0;  # definitionalclasses (single field, without { ... })
     }
     {
       if ($0 ~ "[ ]*Class") {
         startclass = 1;
       }
       if (startclass == 1 && $0 ~ ":=") {
         inclass = 1;
         indefclass = 1;
       }
       if (startclass == 1 && $0 ~ ":=.*{") {
         indefclass = 0;
       }
       if (inclass == 1) startclass = 0;

       if (inclass == 1 && $0 ~ ":>") {
         if ($0 ~ "{ .*:>") {  # first field on a single line
           sub("{ ", "{ #[global] ");
         } else if ($0 ~ ":=.*:>") {  # definitional classes on a single line
           sub(":= ", ":= #[global] ");
         } else if ($0 ~ "^  ") {
           sub("  ", "  #[global] ");
         } else {
           $0 = "#[global] " $0;
         }
         sub(":>", "::")
       }
     print $0;

     if ($0 ~ ".*}[.]" || indefclass == 1 && $0 ~ "[.]$") inclass = 0;
   }

  (`#18590 <https://github.com/coq/coq/pull/18590>`_,
  by Pierre Roux).
- **Changed:**
  Mutually-proved theorems with statements in different coinductive
  types now supported
  (`#18743 <https://github.com/coq/coq/pull/18743>`_,
  by Hugo Herbelin).
- **Added:**
  :cmd:`CoFixpoint` supports attributes `bypass_guard`, `clearbody`,
  `deprecated` and `warn`
  (`#18754 <https://github.com/coq/coq/pull/18754>`_,
  by Hugo Herbelin).
- **Added:**
  `Program Fixpoint` with `measure` or `wf` (see
  :ref:`program_fixpoint`) now supports the `where` clause for
  notations, the `local` and `clearbody` attributes, as well as
  non-atomic conclusions
  (`#18834 <https://github.com/coq/coq/pull/18834>`_,
  by Hugo Herbelin, fixes in particular
  `#13812 <https://github.com/coq/coq/issues/13812>`_ and
  `#14841 <https://github.com/coq/coq/issues/14841>`_).
- **Fixed:**
  Anomaly on the absence of remaining obligations of some name now
  an error
  (`#18873 <https://github.com/coq/coq/pull/18873>`_,
  fixes `#3889 <https://github.com/coq/coq/issues/3889>`_,
  by Hugo Herbelin).
- **Fixed:**
  Universe polymorphic `Program`'s obligations are now generalized
  only over the universe variables that effectively occur in the
  obligation
  (`#18915 <https://github.com/coq/coq/pull/18915>`_,
  fixes `#11766 <https://github.com/coq/coq/issues/11766>`_
  and `#11988 <https://github.com/coq/coq/issues/11988>`_,
  by Hugo Herbelin).
- **Fixed:**
  Anomaly `assertion failed` in pattern-matching compilation, with
  :flag:`Program Mode` or with let-ins in the arity of an inductive type
  (`#18921 <https://github.com/coq/coq/pull/18921>`_,
  fixes `#5777 <https://github.com/coq/coq/issues/5777>`_
  and `#11030 <https://github.com/coq/coq/issues/11030>`_
  and `#11586 <https://github.com/coq/coq/issues/11586>`_,
  by Hugo Herbelin).
- **Fixed:**
  Support for `Program`-style pattern-matching on more than one
  argument in an inductive family
  (`#18929 <https://github.com/coq/coq/pull/18929>`_,
  fixes `#1956 <https://github.com/coq/coq/issues/1956>`_
  and `#5777 <https://github.com/coq/coq/issues/5777>`_,
  by Hugo Herbelin).
- **Fixed:**
  anomaly with obligations in the binders of a `measure`- or
  `wf`-based `Program Fixpoint`
  (`#18958 <https://github.com/coq/coq/pull/18958>`_,
  fixes `#18920 <https://github.com/coq/coq/issues/18920>`_,
  by Hugo Herbelin).
- **Fixed:**
  Incorrect registration of universe names attached to a primitive
  polymorphic constant
  (`#19100 <https://github.com/coq/coq/pull/19100>`_,
  fixes `#19099 <https://github.com/coq/coq/issues/19099>`_,
  by Hugo Herbelin).

Notations
^^^^^^^^^

- **Changed:**
  an :g:`only printing` interpretation of a notation with a specific
  format does no longer change the printing rule of other
  interpretations of the notation; to globally change the default
  printing rule of all interpretations of a notation, use
  :g:`Reserved Notation` instead
  (`#16329 <https://github.com/coq/coq/pull/16329>`_,
  fixes `#16262 <https://github.com/coq/coq/issues/16262>`_,
  by Hugo Herbelin).
- **Changed:**
  levels of :cmd:`Reserved Notation` now default to levels of
  previous notations with longest common prefix, if any. This helps to
  :ref:`factorize notations <NotationFactorization>` with common
  prefixes
  (`#19149 <https://github.com/coq/coq/pull/19149>`_,
  by Pierre Roux).
- **Added:**
  :warn:`closed-notation-not-level-0` and :warn:`postfix-notation-not-level-1`
  warnings about closed and postfix notations at unusual levels
  (`#18588 <https://github.com/coq/coq/pull/18588>`_,
  by Pierre Roux).
- **Added:**
  :warn:`notation-incompatible-prefix` warning when two notation
  definitions have incompatible prefixes
  (`#19049 <https://github.com/coq/coq/pull/19049>`_,
  by Pierre Roux).
- **Fixed:**
  Notations for applied constants equipped with multiple signatures of
  implicit arguments were not correctly inserting as many maximal
  implicit arguments as they should have
  (`#18445 <https://github.com/coq/coq/pull/18445>`_,
  by Hugo Herbelin).
- **Fixed:**
--> --------------------

--> maximum size reached

--> --------------------

Quelle changes.rst Sprache: unbekannt

[ Dauer der Verarbeitung: 0.43 Sekunden (vorverarbeitet) ]