- V8.11.0
-
b7c4ca9 -
Verified
This commit was signed with a verified signature.ppedrot Pierre-Marie Pédrot
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!).
- V8.11+beta1
-
30a4027 -
Verified
This tag was signed with a verified signature.
- V8.11+beta1
-
30a4027 -
Verified
This tag was signed with a verified signature.
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 theCoq.Float.Floatslibrary.
Many other cleanups and improvements have been performed and are further described in the changelog.
Special note on compability:
- Fixed bugs of
ExportandImportthat can have a
significant impact on user developments (common source of
incompatibility!).
Coq 8.10.2 brings a few bug fixes and documentation improvements, in particular:
- Fixed a critical bug of template polymorphism and nonlinear universes
- Fixed a few anomalies
- Fixed an 8.10 regression related to the printing of coercions associated to notations
- Fixed uneven dimensions of CoqIDE panels when window has been resized
- Fixed queries in CoqIDE
More details can be found in the reference manual.
Coq 8.10.1 brings a few bug fixes and documentation improvements, in particular:
- Fix proof of False when using SProp
- Fix an anomaly when unsolved evar in Add Ring
- Fix Ltac regression in binding free names in uconstr
- Fix handling of unicode input before space
- Fix custom extraction of inductives to JSON
Coq 8.10.0 contains:
- some quality-of-life bug fixes;
- a critical bug fix related to template polymorphism;
- native 63-bit machine integers;
- a new sort of definitionally proof-irrelevant propositions: SProp;
- private universes for opaque polymorphic constants;
- string notations and numeral notations;
- a new simplex-based proof engine for the tactics lia, nia, lra and nra;
- new introduction patterns for SSReflect;
- a tactic to rewrite under binders: under;
- easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.
All details can be found in the user manual.
- V8.10+beta3
-
6250503 -
Verified
This tag was signed with a verified signature.vbgl Vincent Laporte
- V8.10+beta3
-
6250503 -
Verified
This tag was signed with a verified signature.
This is the third β version of Coq 8.10.
Compared to the previous one, it includes various bug fixes, including:
- improved warning on coercion path ambiguity;
- support for OCaml extraction of primitive machine integers;
- fix for the soundness issue with template polymorphism;
- fix extraction of dependent record projections to OCaml.
More details are given in the user manual.