coq/coq V8.12.1

Coq 8.12.1

on GitHub

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 (#13330).
• 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 (#12837).
• Several bugs with Search (#13298, #13349).
• The details environment introduced in coqdoc in Coq 8.12 can now be used as advertised in the reference manual (#12772).
• View menu "Display parentheses" introduced in CoqIDE in Coq 8.12 now works correctly (#12793).

See the changelog for details and a more complete list.

New: a macOS installer is now available.