Home

Coq 8.12.1 is out

Submitted by Emilio Gallego Arias and Théo Zimmermann on November 16th, 2020

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.