Home

Coq 8.12.0 is out

Submitted by Emilio Gallego Arias and Théo Zimmermann on July 27th, 2020

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.