Coq 8.12.0 is out

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.