Dear Coq users and contributors,
We are happy to announce the release of Coq 8.12.1.
This release contains numerous bug fixes and documentation improvements. Some bug fix highlights:
- Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency.
- Regression in error reporting after SSReflect’s case tactic. A generic error message “Could not fill dependent hole in apply” was reported for any error following case or elim.
- Several bugs with Search.
- The details environment introduced in coqdoc in Coq 8.12 can now be used as advertised in the reference manual.
- View menu “Display parentheses” introduced in CoqIDE in Coq 8.12 now works correctly.
See the changelog for details and a more complete list: https://coq.inria.fr/refman/changes.html#changes-in-8-12-1
The release is already available in Homebrew and Nix and is coming to opam (see https://github.com/ocaml/opam-repository/pull/17619) and lots of other package managers soon.
Windows and macOS installers can be downloaded from the release page on GitHub: https://github.com/coq/coq/releases/tag/V8.12.1
Note that we are not providing a macOS installer for this release due to infrastructure issues. We hope that this will be alleviated soon by the incoming Coq Platform. In the meantime, macOS users can rely on opam, nix or brew.
Cheers,
The 8.12 release managers, Emilio and Théo