From 0ce7fbb5550ad7a3acc7e06fe9d9bcc24e14ac70 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 8 Jan 2020 14:21:13 +0100 Subject: Changelog for 8.11.0. --- ...1361-fix-11360-discharge-template-param-var.rst | 4 -- .../10657-minim-toset-flex.rst | 3 - ...ing-variable-pattern-matching-decompilation.rst | 6 -- .../03-notations/11276-master+fix10750.rst | 4 -- .../11311-custom-entries-recursive.rst | 5 -- .../04-tactics/10762-notypeclasses-refine.rst | 4 -- .../04-tactics/11203-fix-time-printing.rst | 4 -- doc/changelog/04-tactics/11263-micromega-fix.rst | 6 -- doc/changelog/04-tactics/11337-omega-with-depr.rst | 6 -- .../11241-master+bug-cofix-with-8.10.rst | 4 -- .../11255-master+fix11254-coqtop-version.rst | 4 -- doc/changelog/08-tools/11357-master.rst | 4 -- .../11227-date.rst | 5 -- doc/sphinx/changes.rst | 83 ++++++++++++++++++++++ 14 files changed, 83 insertions(+), 59 deletions(-) delete mode 100644 doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst delete mode 100644 doc/changelog/02-specification-language/10657-minim-toset-flex.rst delete mode 100644 doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst delete mode 100644 doc/changelog/03-notations/11276-master+fix10750.rst delete mode 100644 doc/changelog/03-notations/11311-custom-entries-recursive.rst delete mode 100644 doc/changelog/04-tactics/10762-notypeclasses-refine.rst delete mode 100644 doc/changelog/04-tactics/11203-fix-time-printing.rst delete mode 100644 doc/changelog/04-tactics/11263-micromega-fix.rst delete mode 100644 doc/changelog/04-tactics/11337-omega-with-depr.rst delete mode 100644 doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst delete mode 100644 doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst delete mode 100644 doc/changelog/08-tools/11357-master.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/11227-date.rst diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst deleted file mode 100644 index 8c84648aa7..0000000000 --- a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** `#11360 `_ - Broken section closing when a template polymorphic inductive type depends on - a section variable through its parameters (`#11361 - `_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst b/doc/changelog/02-specification-language/10657-minim-toset-flex.rst deleted file mode 100644 index 8983e162fb..0000000000 --- a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Changed heuristics for universe minimization to :g:`Set`: only - minimize flexible universes (`#10657 `_, - by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau). diff --git a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst b/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst deleted file mode 100644 index 941469d698..0000000000 --- a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - A dependency was missing when looking for default clauses in the - algorithm for printing pattern matching clauses (`#11233 - `_, by Hugo Herbelin, fixing - `#11231 `_, reported by Barry - Jay). diff --git a/doc/changelog/03-notations/11276-master+fix10750.rst b/doc/changelog/03-notations/11276-master+fix10750.rst deleted file mode 100644 index a1b8594f5f..0000000000 --- a/doc/changelog/03-notations/11276-master+fix10750.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - :cmd:`Print Visibility` was failing in the presence of only-printing notations - (`#11276 `_, - by Hugo Herbelin, fixing `#10750 `_). diff --git a/doc/changelog/03-notations/11311-custom-entries-recursive.rst b/doc/changelog/03-notations/11311-custom-entries-recursive.rst deleted file mode 100644 index ae9888512d..0000000000 --- a/doc/changelog/03-notations/11311-custom-entries-recursive.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Recursive notations with custom entries were incorrectly parsing `constr` - instead of custom grammars (`#11311 `_ - by Maxime Dénès, fixes `#9532 `_, - `#9490 `_). diff --git a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst deleted file mode 100644 index 2fef75dc7f..0000000000 --- a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - The tactics :tacn:`eapply`, :tacn:`refine` and its variants no - longer allows shelved goals to be solved by typeclass resolution. - (`#10762 `_, by Matthieu Sozeau). diff --git a/doc/changelog/04-tactics/11203-fix-time-printing.rst b/doc/changelog/04-tactics/11203-fix-time-printing.rst deleted file mode 100644 index cdfd2b228e..0000000000 --- a/doc/changelog/04-tactics/11203-fix-time-printing.rst +++ /dev/null @@ -1,4 +0,0 @@ -- The optional string argument to :tacn:`time` is now properly quoted - under :cmd:`Print Ltac` (`#11203 - `_, fixes `#10971 - `_, by Jason Gross) diff --git a/doc/changelog/04-tactics/11263-micromega-fix.rst b/doc/changelog/04-tactics/11263-micromega-fix.rst deleted file mode 100644 index ebfb6c19b1..0000000000 --- a/doc/changelog/04-tactics/11263-micromega-fix.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed** - Efficiency regression introduced by PR `#9725 `_. - (`#11263 `_, - fixes `#11063 `_, - and `#11242 `_, - and `#11270 `_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11337-omega-with-depr.rst b/doc/changelog/04-tactics/11337-omega-with-depr.rst deleted file mode 100644 index 25e929e030..0000000000 --- a/doc/changelog/04-tactics/11337-omega-with-depr.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Deprecated:** - The undocumented ``omega with`` tactic variant has been deprecated, - using ``lia`` is the recommended replacement, tho the old semantics - of ``omega with *`` can be recovered with ``zify; omega`` - (`#11337 `_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst b/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst deleted file mode 100644 index 462ba4a7b1..0000000000 --- a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Syntax of tactic `cofix ... with ...` was broken from Coq 8.10. - (`#11241 `_, - by Hugo Herbelin). diff --git a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst deleted file mode 100644 index ecc134748d..0000000000 --- a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - ``coqtop --version`` was broken when called in the middle of an installation process - (`#11255 `_, by Hugo Herbelin, fixing - `#11254 `_). diff --git a/doc/changelog/08-tools/11357-master.rst b/doc/changelog/08-tools/11357-master.rst deleted file mode 100644 index 599db5b1da..0000000000 --- a/doc/changelog/08-tools/11357-master.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable - together with an unpacked (``mllib``) plugin. (`#11357 - `_, by Gaëtan Gilbert). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst b/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst deleted file mode 100644 index 5c08e2b0ea..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` - environment variable - (`#11227 `_, - by Bernhard M. Wiedemann). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 21000889d3..a1410b0412 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -514,6 +514,89 @@ Changes in 8.11+beta1 (`#10471 `_, by Emilio Jesús Gallego Arias). +Changes in 8.11.0 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Fixed:** `#11360 `_. + Broken section closing when a template polymorphic inductive type depends on + a section variable through its parameters (`#11361 + `_, by Gaëtan Gilbert). + +**Specification language, type inference** + +- **Changed:** Heuristics for universe minimization to :g:`Set`: only + minimize flexible universes (`#10657 `_, + by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau). +- **Fixed:** + A dependency was missing when looking for default clauses in the + algorithm for printing pattern matching clauses (`#11233 + `_, by Hugo Herbelin, fixing + `#11231 `_, reported by Barry + Jay). + +**Notations** + +- **Fixed:** + :cmd:`Print Visibility` was failing in the presence of only-printing notations + (`#11276 `_, + by Hugo Herbelin, fixing `#10750 `_). +- **Fixed:** + Recursive notations with custom entries were incorrectly parsing `constr` + instead of custom grammars (`#11311 `_ + by Maxime Dénès, fixes `#9532 `_, + `#9490 `_). + +**Tactics** + +- **Changed:** + The tactics :tacn:`eapply`, :tacn:`refine` and variants no + longer allow shelved goals to be solved by typeclass resolution + (`#10762 `_, by Matthieu Sozeau). +- **Fixed:** The optional string argument to :tacn:`time` is now + properly quoted under :cmd:`Print Ltac` (`#11203 + `_, fixes `#10971 + `_, by Jason Gross) +- **Fixed:** + Efficiency regression introduced by PR `#9725 `_ + (`#11263 `_, + fixes `#11063 `_, + and `#11242 `_, + and `#11270 `_, by Frédéric Besson). +- **Deprecated:** + The undocumented ``omega with`` tactic variant has been deprecated. + Using ``lia`` is the recommended replacement, tho the old semantics + of ``omega with *`` can be recovered with ``zify; omega`` + (`#11337 `_, + by Emilio Jesus Gallego Arias). + +**Tactic language** + +- **Fixed:** + Syntax of tactic `cofix ... with ...` was broken from Coq 8.10. + (`#11241 `_, + by Hugo Herbelin). + +**Tools** + +- **Fixed:** + ``coqtop --version`` was broken when called in the middle of an installation process + (`#11255 `_, by Hugo Herbelin, fixing + `#11254 `_). +- **Fixed:** + ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable + together with an unpacked (``mllib``) plugin. (`#11357 + `_, by Gaëtan Gilbert). + +**Infrastructure and dependencies** + +- **Added:** + Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` + environment variable + (`#11227 `_, + by Bernhard M. Wiedemann). + Version 8.10 ------------ -- cgit v1.2.3