Stay up to date on releases
Create your free account today to subscribe to this repository for notifications about new releases, and build software alongside 40 million developers on GitHub.
Sign up for free See pricing for teams and enterprises
The main changes brought by Coq version 8.11 are:
- 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 theCoq.Float.Floatslibrary.
Many other cleanups and improvements have been performed and are further described in the changelog.
Special note on compatibility:
- Fixed bugs of
ExportandImportthat can have a
significant impact on user developments (common source of
incompatibility!).