Coq 8.12.1 is out

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.