# Coq 8.12.0 is out!

**URL:** <https://discourse.rocq-prover.org/t/coq-8-12-0-is-out/972>\
**Category:** Announcements\
**Created:** [July 27, 2020, 6:04pm UTC](https://discourse.rocq-prover.org/t/coq-8-12-0-is-out/972 "2020-07-27T18:04:16Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [July 27, 2020, 6:04pm UTC](https://discourse.rocq-prover.org/t/coq-8-12-0-is-out/972/1 "2020-07-27T18:04:16Z")

</div>

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](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/](https://hub.docker.com/r/coqorg/coq/)).

You may find the Windows and macOS installers on GitHub:

> **[Release Coq 8.12.0 · coq/coq](https://github.com/coq/coq/releases/tag/V8.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 libra...

The 8.12 release managers, Emilio and Théo, and the whole Coq development team