From a6b5a5a66b59750148ead34148cfefd1702a64e0 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 5 Nov 2020 16:47:36 +0100 Subject: Changelog for 8.12.1. --- .../01-kernel/12738-fix-sr-cumul-inds.rst | 5 - ...08-part1-collision-lonely-notation-printing.rst | 6 -- ...026-master+fix-printing-custom-no-level-8.2.rst | 7 -- ...ster+fix-display-parentheses-default-coqide.rst | 5 - ...6-master+fix12787-K-redex-injection-anomaly.rst | 6 -- ...2847-master+inversion-works-with-eq-in-type.rst | 6 -- ...master+fix13241-locating-nested-ltac-errors.rst | 6 -- .../06-ssreflect/12857-changelog-for-12857.rst | 8 -- ...x13298-bad-env-search-primitive-projections.rst | 5 - .../12754-master+fix-coqdoc-index-escaping.rst | 6 -- doc/changelog/08-tools/12772-fix-details.rst | 5 - .../13063-fix-no-output-sync-make-file.rst | 6 -- .../12864-fix-approve-output.rst | 5 - .../12972-ocaml+4_11.rst | 4 - .../13011-sphinx-3.rst | 5 - doc/sphinx/changes.rst | 113 ++++++++++++++++++++- 16 files changed, 110 insertions(+), 88 deletions(-) delete mode 100644 doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst delete mode 100644 doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst delete mode 100644 doc/changelog/03-notations/13026-master+fix-printing-custom-no-level-8.2.rst delete mode 100644 doc/changelog/03-notations/13067-master+fix-display-parentheses-default-coqide.rst delete mode 100644 doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst delete mode 100644 doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst delete mode 100644 doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst delete mode 100644 doc/changelog/06-ssreflect/12857-changelog-for-12857.rst delete mode 100644 doc/changelog/07-commands-and-options/13301-master+fix13298-bad-env-search-primitive-projections.rst delete mode 100644 doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst delete mode 100644 doc/changelog/08-tools/12772-fix-details.rst delete mode 100644 doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst diff --git a/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst b/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst deleted file mode 100644 index 1bf62de3fd..0000000000 --- a/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** Incompleteness of conversion checking on problems - involving :ref:`eta-expansion` and :ref:`cumulative universe - polymorphic inductive types ` (`#12738 - `_, fixes `#7015 - `_, by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst b/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst deleted file mode 100644 index 95a9093272..0000000000 --- a/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Undetected collision between a lonely notation and a notation in - scope at printing time - (`#12946 `_, - fixes the first part of `#12908 `_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/13026-master+fix-printing-custom-no-level-8.2.rst b/doc/changelog/03-notations/13026-master+fix-printing-custom-no-level-8.2.rst deleted file mode 100644 index 42b62eed75..0000000000 --- a/doc/changelog/03-notations/13026-master+fix-printing-custom-no-level-8.2.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Fixed:** - Fixing printing of notations in custom entries with - variables not mentioning an explicit level - (`#13026 `_, - fixes `#12775 `_ - and `#13018 `_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/13067-master+fix-display-parentheses-default-coqide.rst b/doc/changelog/03-notations/13067-master+fix-display-parentheses-default-coqide.rst deleted file mode 100644 index 50aa4a9052..0000000000 --- a/doc/changelog/03-notations/13067-master+fix-display-parentheses-default-coqide.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Repairing option :g:`Display parentheses` in CoqIDE - (`#12794 `_ and `#13067 `_, - fixes `#12793 `_, - by Jean-Christophe Léchenet and Hugo Herbelin). diff --git a/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst b/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst deleted file mode 100644 index 289d17167d..0000000000 --- a/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Anomaly with :tacn:`injection` involving artificial - dependencies disappearing by reduction - (`#12816 `_, - fixes `#12787 `_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst b/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst deleted file mode 100644 index b444a2f436..0000000000 --- a/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - :tacn:`replace` and :tacn:`inversion` support registration of a - :g:`core.identity`-like equality in :g:`Type`, such as HoTT's :g:`path` - (`#12847 `_, - partially fixes `#12846 `_, - by Hugo Herbelin). diff --git a/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst b/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst deleted file mode 100644 index 1eb8ef5a2a..0000000000 --- a/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Miscellaneous issues with locating tactic errors - (`#13247 `_, - fixes `#12773 `_ - and `#12992 `_, - by Hugo Herbelin). diff --git a/doc/changelog/06-ssreflect/12857-changelog-for-12857.rst b/doc/changelog/06-ssreflect/12857-changelog-for-12857.rst deleted file mode 100644 index 4350fd0238..0000000000 --- a/doc/changelog/06-ssreflect/12857-changelog-for-12857.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - Regression in error reporting after :tacn:`case `. - A generic error message "Could not fill dependent hole in apply" was - reported for any error following :tacn:`case ` or - :tacn:`elim ` - (`#12857 `_, - fixes `#12837 `_, - by Enrico Tassi). diff --git a/doc/changelog/07-commands-and-options/13301-master+fix13298-bad-env-search-primitive-projections.rst b/doc/changelog/07-commands-and-options/13301-master+fix13298-bad-env-search-primitive-projections.rst deleted file mode 100644 index 97ea1b9aa9..0000000000 --- a/doc/changelog/07-commands-and-options/13301-master+fix13298-bad-env-search-primitive-projections.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Failures of :cmd:`Search` in the presence of primitive projections - (`#13301 `_, - fixes `#13298 `_, - by Hugo Herbelin). diff --git a/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst b/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst deleted file mode 100644 index a05829b720..0000000000 --- a/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Special symbols now escaped in the index produced by coqdoc, - avoiding collision with the syntax of the output format - (`#12754 `_, - fixes `#12752 `_, - by Hugo Herbelin). diff --git a/doc/changelog/08-tools/12772-fix-details.rst b/doc/changelog/08-tools/12772-fix-details.rst deleted file mode 100644 index 67ee061285..0000000000 --- a/doc/changelog/08-tools/12772-fix-details.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - The `details` environment added in the 8.12 release can now be used - as advertised in the reference manual - (`#12772 `_, - by Thomas Letan). diff --git a/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst b/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst deleted file mode 100644 index 75b1e26248..0000000000 --- a/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Targets such as ``print-pretty-timed`` in ``coq_makefile``-made - ``Makefile``\s no longer error in rare cases where ``--output-sync`` is not - passed to make and the timing output gets interleaved in just the wrong way - (`#13063 `_, fixes `#13062 - `_, by Jason Gross). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst b/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst deleted file mode 100644 index c754826e62..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - ``make approve-output`` in the test-suite now correctly handles - ``output-coqtop`` and ``output-coqchk`` tests (`#12864 - `_, fixes `#12863 - `_, by Jason Gross). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst b/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst deleted file mode 100644 index 855aa360f1..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Coq is now tested against OCaml 4.11.1 - (`#12972 `_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst b/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst deleted file mode 100644 index d17a2dff6b..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - The reference manual can now build with Sphinx 3 - (`#13011 `_, - fixes `#12332 `_, - by Théo Zimmermann and Jim Fehrle). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5bc229954f..79f00a4a5a 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -1141,9 +1141,6 @@ Infrastructure and dependencies Changes in 8.12.0 ~~~~~~~~~~~~~~~~~~~~~ -.. contents:: - :local: - **Notations** - **Added:** @@ -1216,6 +1213,116 @@ Changes in 8.12.0 modified in the meantime (`#12583 `_, fixes `#12582 `_, by Jason Gross). +Changes in 8.12.1 +~~~~~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Fixed:** Incompleteness of conversion checking on problems + involving :ref:`eta-expansion` and :ref:`cumulative universe + polymorphic inductive types ` (`#12738 + `_, fixes `#7015 + `_, by Gaëtan Gilbert). + +**Notations** + +- **Fixed:** + Undetected collision between a lonely notation and a notation in + scope at printing time + (`#12946 `_, + fixes the first part of `#12908 `_, + by Hugo Herbelin). +- **Fixed:** + Printing of notations in custom entries with + variables not mentioning an explicit level + (`#13026 `_, + fixes `#12775 `_ + and `#13018 `_, + by Hugo Herbelin). + +**Tactics** + +- **Added:** + :tacn:`replace` and :tacn:`inversion` support registration of a + :g:`core.identity`\-like equality in :g:`Type`, such as HoTT's :g:`path` + (`#12847 `_, + partially fixes `#12846 `_, + by Hugo Herbelin). +- **Fixed:** + Anomaly with :tacn:`injection` involving artificial + dependencies disappearing by reduction + (`#12816 `_, + fixes `#12787 `_, + by Hugo Herbelin). + +**Tactic language** + +- **Fixed:** + Miscellaneous issues with locating tactic errors + (`#13247 `_, + fixes `#12773 `_ + and `#12992 `_, + by Hugo Herbelin). + +**SSReflect** + +- **Fixed:** + Regression in error reporting after :tacn:`case `. + A generic error message "Could not fill dependent hole in apply" was + reported for any error following :tacn:`case ` or + :tacn:`elim ` + (`#12857 `_, + fixes `#12837 `_, + by Enrico Tassi). + +**Commands and options** + +- **Fixed:** + Failures of :cmd:`Search` in the presence of primitive projections + (`#13301 `_, + fixes `#13298 `_, + by Hugo Herbelin). + +**Tools** + +- **Fixed:** + Special symbols now escaped in the index produced by coqdoc, + avoiding collision with the syntax of the output format + (`#12754 `_, + fixes `#12752 `_, + by Hugo Herbelin). +- **Fixed:** + The `details` environment added in the 8.12 release can now be used + as advertised in the reference manual + (`#12772 `_, + by Thomas Letan). +- **Fixed:** + Targets such as ``print-pretty-timed`` in ``coq_makefile``\-made + ``Makefile``\s no longer error in rare cases where ``--output-sync`` is not + passed to make and the timing output gets interleaved in just the wrong way + (`#13063 `_, fixes `#13062 + `_, by Jason Gross). + +**CoqIDE** + +- **Fixed:** + View menu "Display parentheses" + (`#12794 `_ and `#13067 `_, + fixes `#12793 `_, + by Jean-Christophe Léchenet and Hugo Herbelin). + +**Infrastructure and dependencies** + +- **Added:** + Coq is now tested against OCaml 4.11.1 + (`#12972 `_, + by Emilio Jesus Gallego Arias). +- **Fixed:** + The reference manual can now build with Sphinx 3 + (`#13011 `_, + fixes `#12332 `_, + by Théo Zimmermann and Jim Fehrle). + Version 8.11 ------------ -- cgit v1.2.3