Dear Coq community,
the Coq development team is proud to announce the immediate
availability of the Coq Platform version 2021.02.1, based on Coq
The Coq platform is a distribution of the Coq proof assistant together
with a selection of Coq libraries. See  for the project homepage,
and  for the new instructions for getting Coq.
For expert users it provides a set of scripts to compile and install
OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and
many Linux distributions in a reliable and extensible way with
For beginners it provides easy to use binary installers for Windows,
MacOS and Linux.
The next point releases, starting with 2021.02.2, will focus on
including more Coq libraries (and no breaking change).
Highlights for Coq version 8.13.2:
- Fix crash when using vm_compute on an irreducible PArray.set
- Fix crash when loading .vo files containing a vm_compute
normalized primitive array
- Fix Ltac2.Array.init computational complexity
Highlights for the Coq Platform version 2021.02.1:
- DMG installer package for macOS
- Homotopy Type Theory library version 8.13
- The Verified Software Toolchain updated to 2.7.1
Enrico Tassi for the Coq Team