Coq 8.11.0 is out

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.