Dear Coq users,
We are happy to announce the release of Coq 8.12.0.
Some highlights from this release are:
- a new binder notation for non-maximal implicit arguments;
- an improved Search command which accepts more complex queries;
- many additions to the standard library;
- a restructured reference manual;
- the deprecation of the omega tactic in favor the lia tactic.
Please see the changelog to learn more about this release:
https://coq.github.io/doc/v8.12/refman/changes.html#version-8-12
Thanks to the reactivity of Coq users, this version is already
available in many packaging systems. In particular, it is already
available on opam and as a Docker image
(https://hub.docker.com/r/coqorg/coq/).
You may find the Windows and macOS installers on GitHub:
The 8.12 release managers, Emilio and Théo, and the whole Coq development team