Coq 8.10.0 was released, and it uses GTK+3 instead of GTK+2 for CoqIDE. https://github.com/coq/coq/releases/tag/V8.10.0 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.
Coq 8.10.2 was released on 30.11.2019 https://github.com/coq/coq/releases/tag/V8.10.2 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
Coq 8.11.2 was released, and it supports OCaml 4.10.0. https://github.com/coq/coq/releases/tag/V8.11.2 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.
Coq 8.12.0 was released: https://github.com/coq/coq/releases/tag/V8.12.0 Some highlights from this release are: - a new binder notation for non-maximal implicit arguments; - an improved Search command which accepts more complex queries; - many additions to the standard library; - a restructured reference manual; - the deprecation of the omega tactic in favor the lia tactic.
The bug has been closed via the following commit(s): https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=1ebf1913a56ae24bc2c951ac1080f58904f7944a commit 1ebf1913a56ae24bc2c951ac1080f58904f7944a Author: Mark Wright <gienah@gentoo.org> AuthorDate: 2020-10-13 12:30:31 +0000 Commit: Mark Wright <gienah@gentoo.org> CommitDate: 2020-10-13 12:53:49 +0000 sci-mathematics/coq: Bump to 8.12.0 Thanks to Anton Kochkov and Sergio Perez for reporting. Closes: https://bugs.gentoo.org/697066 Package-Manager: Portage-3.0.8, Repoman-3.0.1 Signed-off-by: Mark Wright <gienah@gentoo.org> sci-mathematics/coq/Manifest | 1 + sci-mathematics/coq/coq-8.12.0.ebuild | 88 +++++++++++++++++++++++++++++++++++ 2 files changed, 89 insertions(+)
