Skip to content
Compare
Choose a tag to compare

Coq 8.11+β1

Pre-release
Pre-release
@ppedrot ppedrot released this
· 372 commits to v8.11 since this release
V8.11+beta1
30a4027
Compare
Choose a tag to compare

This is the first β version of Coq 8.11.

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 the Coq.Float.Floats library.

Many other cleanups and improvements have been performed and are further described in the changelog.

Special note on compability:

  • Fixed bugs of Export and Import that can have a
    significant impact on user developments (common source of
    incompatibility!
    ).