From 254efbe77e9c7b9dfefe52825ed062c202060507 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 27 Nov 2019 14:53:44 +0000 Subject: Release notes for Coq 8.10.2 --- ...090-master+refactoring-application-printing.rst | 3 -- doc/sphinx/changes.rst | 47 +++++++++++++++++++++- 2 files changed, 46 insertions(+), 4 deletions(-) delete mode 100644 doc/changelog/03-notations/11090-master+refactoring-application-printing.rst diff --git a/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst deleted file mode 100644 index 4423c2b587..0000000000 --- a/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Fixed an 8.10 regression related to the printing of coercions associated to notations - (`#11090 `_, - fixes ` #11033 `_, by Hugo Herbelin). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 80a24b997c..01db9da03b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -568,7 +568,7 @@ Other changes in 8.10+beta1 - The prelude used to be automatically Exported and is now only Imported. This should be relevant only when importing files which don't use `-noinit` into files which do - (`#9013 `_, by Gaëtan Gilert). + (`#9013 `_, by Gaëtan Gilbert). - Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an ordered type, using lexical order @@ -765,6 +765,51 @@ A few bug fixes and documentation improvements, in particular: fixes `#4741 `_, by Helge Bahmann). +Changes in 8.10.2 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- Fixed a critical bug of template polymorphism and nonlinear universes + (`#11128 `_, + fixes `#11039 `_, + by Gaëtan Gilbert). + +- Fixed an anomaly “Uncaught exception Constr.DestKO” on :g:`Inductive` + (`#11052 `_, + fixes `#11048 `_, + by Gaëtan Gilbert). + +- Fixed an anomaly “not enough abstractions in fix body” + (`#11014 `_, + fixes `#8459 `_, + by Gaëtan Gilbert). + +**Notations** + +- Fixed an 8.10 regression related to the printing of coercions associated to notations + (`#11090 `_, + fixes `#11033 `_, by Hugo Herbelin). + +**CoqIDE** + +- Fixed uneven dimensions of CoqIDE panels when window has been resized + (`#11070 `_, + fixes 8.10-regression `#10956 `_, + by Guillaume Melquiond). + +- Do not include final stops in queries + (`#11069 `_, + fixes 8.10-regression `#11058 `_, + by Guillaume Melquiond). + +**Infrastructure and dependencies** + +- Enable building of executables when they are running + (`#11000 `_, + fixes 8.9-regression `#10728 `_, + by Gaëtan Gilbert). + Version 8.9 ----------- -- cgit v1.2.3