We are proud to announce the immediate availability of Coq 8.20. This
version 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. This release has been made
possible thanks to the work of dozens of contributors and reviewers,
see the [changelog](Recent changes — Coq 8.20.0 documentation)
for full credits and detail of changes.
Coq 8.20 is available, along with a number of libraries, as OPAM and
Nix packages or in a Docker image.
Pierre and Guilaume, on behalf of the Coq development team