Merge PR #13311: Changelog for 8.12.1.

Reviewed-by: ejgallego

16 files changed, 110 insertions, 88 deletions

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 <cumulative>` (`#12738
-  <https://github.com/coq/coq/pull/12738>`_, fixes `#7015
-  <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/12946>`_,
-  fixes the first part of `#12908 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/13026>`_,
-  fixes `#12775 <https://github.com/coq/coq/issues/12775>`_
-  and `#13018 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/12794>`_ and `#13067 <https://github.com/coq/coq/pull/13067>`_,
-  fixes `#12793 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/12816>`_,
-  fixes `#12787 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/12847>`_,
-  partially fixes `#12846 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/13247>`_,
-  fixes `#12773 <https://github.com/coq/coq/issues/12773>`_
-  and `#12992 <https://github.com/coq/coq/issues/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 <case (ssreflect)>`.
-  A generic error message "Could not fill dependent hole in apply" was
-  reported for any error following :tacn:`case <case (ssreflect)>` or
-  :tacn:`elim <elim (ssreflect)>`
-  (`#12857 <https://github.com/coq/coq/pull/12857>`_,
-  fixes `#12837 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/13301>`_,
-  fixes `#13298 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/12754>`_,
-  fixes `#12752 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/13063>`_, fixes `#13062
-  <https://github.com/coq/coq/issues/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
-  <https://github.com/coq/coq/pull/12864>`_, fixes `#12863
-  <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/13011>`_,
-  fixes `#12332 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/12583>`_,
   fixes `#12582 <https://github.com/coq/coq/issues/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 <cumulative>` (`#12738
+  <https://github.com/coq/coq/pull/12738>`_, fixes `#7015
+  <https://github.com/coq/coq/issues/7015>`_, by Gaëtan Gilbert).
+
+**Notations**
+
+- **Fixed:**
+  Undetected collision between a lonely notation and a notation in
+  scope at printing time
+  (`#12946 <https://github.com/coq/coq/pull/12946>`_,
+  fixes the first part of `#12908 <https://github.com/coq/coq/issues/12908>`_,
+  by Hugo Herbelin).
+- **Fixed:**
+  Printing of notations in custom entries with
+  variables not mentioning an explicit level
+  (`#13026 <https://github.com/coq/coq/pull/13026>`_,
+  fixes `#12775 <https://github.com/coq/coq/issues/12775>`_
+  and `#13018 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/12847>`_,
+  partially fixes `#12846 <https://github.com/coq/coq/issues/12846>`_,
+  by Hugo Herbelin).
+- **Fixed:**
+  Anomaly with :tacn:`injection` involving artificial
+  dependencies disappearing by reduction
+  (`#12816 <https://github.com/coq/coq/pull/12816>`_,
+  fixes `#12787 <https://github.com/coq/coq/issues/12787>`_,
+  by Hugo Herbelin).
+
+**Tactic language**
+
+- **Fixed:**
+  Miscellaneous issues with locating tactic errors
+  (`#13247 <https://github.com/coq/coq/pull/13247>`_,
+  fixes `#12773 <https://github.com/coq/coq/issues/12773>`_
+  and `#12992 <https://github.com/coq/coq/issues/12992>`_,
+  by Hugo Herbelin).
+
+**SSReflect**
+
+- **Fixed:**
+  Regression in error reporting after :tacn:`case <case (ssreflect)>`.
+  A generic error message "Could not fill dependent hole in apply" was
+  reported for any error following :tacn:`case <case (ssreflect)>` or
+  :tacn:`elim <elim (ssreflect)>`
+  (`#12857 <https://github.com/coq/coq/pull/12857>`_,
+  fixes `#12837 <https://github.com/coq/coq/issues/12837>`_,
+  by Enrico Tassi).
+
+**Commands and options**
+
+- **Fixed:**
+  Failures of :cmd:`Search` in the presence of primitive projections
+  (`#13301 <https://github.com/coq/coq/pull/13301>`_,
+  fixes `#13298 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/12754>`_,
+  fixes `#12752 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/13063>`_, fixes `#13062
+  <https://github.com/coq/coq/issues/13062>`_, by Jason Gross).
+
+**CoqIDE**
+
+- **Fixed:**
+  View menu "Display parentheses"
+  (`#12794 <https://github.com/coq/coq/pull/12794>`_ and `#13067 <https://github.com/coq/coq/pull/13067>`_,
+  fixes `#12793 <https://github.com/coq/coq/issues/12793>`_,
+  by Jean-Christophe Léchenet and Hugo Herbelin).
+
+**Infrastructure and dependencies**
+
+- **Added:**
+  Coq is now tested against OCaml 4.11.1
+  (`#12972 <https://github.com/coq/coq/pull/12972>`_,
+  by Emilio Jesus Gallego Arias).
+- **Fixed:**
+  The reference manual can now build with Sphinx 3
+  (`#13011 <https://github.com/coq/coq/pull/13011>`_,
+  fixes `#12332 <https://github.com/coq/coq/issues/12332>`_,
+  by Théo Zimmermann and Jim Fehrle).
+
 Version 8.11
 ------------