Coq 8.11+beta1 is out
The first beta release of Coq 8.11 is available for testing.
There are two main changes brought by Coq version 8.11. First, 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. Second, 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.
Feedback and bug reports are extremely welcome.