Coq 8.11.0 is out
Submitted by Pierre-Marie Pédrot on January 28th, 2020
The 8.11.0 release of Coq is available.
There are two main changes brought by Coq 8.11.
- It introduces Ltac2, a new tactic language for writing more robust larger scale tactics, with built-in support for datatypes and the multi-goal tactic monad.
- Primitive floats are integrated in terms and follow the binary64 format of the IEEE 754 standard, as specified in the `Coq.Float.Floats` library.
Many other cleanups and improvements have been performed and are further described in the reference manual.