Skip to content

Coq 8.12.1

Choose a tag to compare
@Zimmi48 Zimmi48 released this 16 Nov 13:39
· 16 commits to v8.12 since this release

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.