Some highlights from this release are:
- a new binder notation for non-maximal implicit arguments;
- an improved
Searchcommand which accepts more complex queries;
- many additions to the standard library;
- a restructured reference manual;
- the deprecation of the
omegatactic in favor the
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.