Highlights:
- Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays.
- Introduction of definitional proof irrelevance for the equality type defined in the SProp sort.
- Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior.
See the changelog for an overview of the new features and changes.
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.
Update: The OSX bundle was regenerated in order to include the missing file libgmp