rocq-prover/rocq V8.12.0

Coq 8.12.0

on GitHub

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.

Notes regarding the macOS installer

This installer is only compatible with macOS 10.13 or higher. Because the application is signed but not "notarized", on macOS 10.15 (Catalina), it won't open by default, unless you right-click and chose "Open". Cf. coq/platform#51 to learn more.