Merge PR #11372: Changelog for 8.11.0.

Reviewed-by: ppedrot

21 files changed, 135 insertions, 100 deletions

diff --git a/doc/changelog/01-kernel/11081-native-cleanup.rst b/doc/changelog/01-kernel/11081-native-cleanup.rst
deleted file mode 100644
index b3e3a78b96..0000000000
--- a/doc/changelog/01-kernel/11081-native-cleanup.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Changed:** the native compilation (:tacn:`native_compute`) now
-  creates a directory to contain temporary files instead of putting
-  them in the root of the system temporary directory. (`#11081
-  <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert).
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 <https://github.com/issues/11360>`_
-  Broken section closing when a template polymorphic inductive type depends on
-  a section variable through its parameters (`#11361
-  <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/01-kernel/11422-Setplus2.rst b/doc/changelog/01-kernel/11422-Setplus2.rst
deleted file mode 100644
index cc174358cc..0000000000
--- a/doc/changelog/01-kernel/11422-Setplus2.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Fixed:**
-  The type of :g:`Set+1` would be computed to be itself, leading to a proof of False.
-  (`#11422 <https://github.com/coq/coq/pull/11422>`_,
-  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 <https://github.com/coq/coq/pull/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
-  <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing
-  `#11231 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/11276>`_,
-  by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/11311>`_
-  by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_,
-  `#9490 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/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
-  <https://github.com/coq/coq/pull/11203>`_, fixes `#10971
-  <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/9725>`_.
-  (`#11263 <https://github.com/coq/coq/pull/11263>`_,
-  fixes `#11063 <https://github.com/coq/coq/issues/11063>`_,
-  and `#11242 <https://github.com/coq/coq/issues/11242>`_,
-  and `#11270 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/11241>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst b/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst
deleted file mode 100644
index a43e950bff..0000000000
--- a/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Deprecated:**
-  The `-load-ml-source` and `-load-ml-object` command line options
-  have been deprecated; their use was very limited, you can achieve the same adding
-  additional object files in the linking step or by using a plugin.
-  (`#11428 <https://github.com/coq/coq/pull/11428>`_,
-  by Emilio Jesus Gallego Arias).
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 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing
-  `#11254 <https://github.com/coq/coq/pull/11254>`_).
diff --git a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst
deleted file mode 100644
index 97f456036d..0000000000
--- a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Deprecated:**
-  The ``-quick`` command is renamed to ``-vio``, for consistency with the new ``-vos`` and ``-vok`` flags. Usage of ``-quick`` is now deprecated.
-  (`#11280 <https://github.com/coq/coq/pull/11280>`_,
-  by charguer).
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
-  <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst b/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst
deleted file mode 100644
index 10952c6b2c..0000000000
--- a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints
-  commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_,
-  fixes `#11353 <https://github.com/coq/coq/issues/11353>`_,
-  by Karl Palmskog).
diff --git a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst b/doc/changelog/09-coqide/11400-gtk-ide-completion.rst
deleted file mode 100644
index 2dc3992b9c..0000000000
--- a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  CoqIDE now uses the GtkSourceView native implementation of
-  the autocomplete mechanism.
-  (`#11400 <https://github.com/coq/coq/pull/11400>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst b/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst
deleted file mode 100644
index 3e1f1e02a4..0000000000
--- a/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Removed:**
-  Export of module ``RList`` in ``Ranalysis.v`` and ``Ranalysis_reg.v``. Module ``RList`` is still there but must be imported explicitly where required.
-  (`#11396 <https://github.com/coq/coq/pull/11396>`_,
-  by Michael Soegtrop).
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 <https://github.com/coq/coq/pull/11227>`_,
-  by Bernhard M. Wiedemann).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 21000889d3..294f121cf8 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -55,23 +55,23 @@ this version of Coq, it should soon be the case and we already
 recommend users to switch to :tacn:`lia` in new proof scripts (see
 also the warning message in the :ref:`corresponding chapter <omega>`).
 
-The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq|
-and affected releases. See the `Changes in 8.11+beta1`_ section for the
-detailed list of changes, including potentially breaking changes marked with
-**Changed**.
+The ``dev/doc/critical-bugs`` file documents the known critical bugs
+of |Coq| and affected releases. See the `Changes in 8.11+beta1`_
+section and following sections for the detailed list of changes,
+including potentially breaking changes marked with **Changed**.
 
 Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael
 Soegtrop, Théo Zimmermann worked on maintaining and improving the
 continuous integration system and package building infrastructure.
 
-Coq's documentation is available at https://coq.github.io/doc/V8.11+beta1/api (documentation of
-the ML API), https://coq.github.io/doc/V8.11+beta1/refman (reference
-manual), and https://coq.github.io/doc/V8.11+beta1/stdlib (documentation of
+Coq's documentation is available at https://coq.github.io/doc/v8.11/api (documentation of
+the ML API), https://coq.github.io/doc/v8.11/refman (reference
+manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of
 the standard library).
 
 The OPAM repository for |Coq| packages has been maintained by
-Karl Palmskog, Matthieu Sozeau, Enrico Tassi with contributions
-from many users. A list of packages is available at
+Guillaume Claret, Karl Palmskog, Matthieu Sozeau, Enrico Tassi with
+contributions from many users. A list of packages is available at
 https://coq.inria.fr/opam/www/.
 
 The 61 contributors to this version are Michael D. Adams, Guillaume
@@ -514,6 +514,132 @@ Changes in 8.11+beta1
   (`#10471 <https://github.com/coq/coq/pull/10471>`_,
   by Emilio Jesús Gallego Arias).
 
+Changes in 8.11.0
+~~~~~~~~~~~~~~~~~
+
+**Kernel**
+
+- **Changed:** the native compilation (:tacn:`native_compute`) now
+  creates a directory to contain temporary files instead of putting
+  them in the root of the system temporary directory (`#11081
+  <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert).
+- **Fixed:** `#11360 <https://github.com/issues/11360>`_.
+  Broken section closing when a template polymorphic inductive type depends on
+  a section variable through its parameters (`#11361
+  <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert).
+- **Fixed:** The type of :g:`Set+1` would be computed to be itself,
+  leading to a proof of False (`#11422
+  <https://github.com/coq/coq/pull/11422>`_, by Gaëtan Gilbert).
+
+**Specification language, type inference**
+
+- **Changed:** Heuristics for universe minimization to :g:`Set`: only
+  minimize flexible universes (`#10657 <https://github.com/coq/coq/pull/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
+  <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing
+  `#11231 <https://github.com/coq/coq/pull/11231>`_, reported by Barry
+  Jay).
+
+**Notations**
+
+- **Fixed:**
+  :cmd:`Print Visibility` was failing in the presence of only-printing notations
+  (`#11276 <https://github.com/coq/coq/pull/11276>`_,
+  by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_).
+- **Fixed:**
+  Recursive notations with custom entries were incorrectly parsing `constr`
+  instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_
+  by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_,
+  `#9490 <https://github.com/coq/coq/pull/9490>`_).
+
+**Tactics**
+
+- **Changed:**
+  The tactics :tacn:`eapply`, :tacn:`refine` and variants no
+  longer allow shelved goals to be solved by typeclass resolution
+  (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau).
+- **Fixed:** The optional string argument to :tacn:`time` is now
+  properly quoted under :cmd:`Print Ltac` (`#11203
+  <https://github.com/coq/coq/pull/11203>`_, fixes `#10971
+  <https://github.com/coq/coq/issues/10971>`_, by Jason Gross)
+- **Fixed:**
+  Efficiency regression introduced by  PR `#9725 <https://github.com/coq/coq/pull/9725>`_
+  (`#11263 <https://github.com/coq/coq/pull/11263>`_,
+  fixes `#11063 <https://github.com/coq/coq/issues/11063>`_,
+  and `#11242 <https://github.com/coq/coq/issues/11242>`_,
+  and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson).
+- **Deprecated:**
+  The undocumented ``omega with`` tactic variant has been deprecated.
+  Using :tacn:`lia` is the recommended replacement, tho the old semantics
+  of ``omega with *`` can be recovered with ``zify; omega``
+  (`#11337 <https://github.com/coq/coq/pull/11337>`_,
+  by Emilio Jesus Gallego Arias).
+- **Fixed**
+  For compatibility reasons, in 8.11, :tacn:`zify` does not support :g:`Z.pow_pos` by default.
+  It can be enabled by loading explicitly the module :g:`ZifyPow`.
+  (`#11430 <https://github.com/coq/coq/pull/11430>`_ by Frédéric Besson
+  fixes `#11191 <https://github.com/coq/coq/issues/11191>`_).
+
+**Tactic language**
+
+- **Fixed:**
+  Syntax of tactic `cofix ... with ...` was broken from Coq 8.10
+  (`#11241 <https://github.com/coq/coq/pull/11241>`_,
+  by Hugo Herbelin).
+
+**Commands and options**
+
+- **Deprecated:** The `-load-ml-source` and `-load-ml-object` command
+  line options have been deprecated; their use was very limited, you
+  can achieve the same by adding object files in the linking step or
+  by using a plugin (`#11428
+  <https://github.com/coq/coq/pull/11428>`_, by Emilio Jesus Gallego
+  Arias).
+
+**Tools**
+
+- **Fixed:**
+  ``coqtop --version`` was broken when called in the middle of an installation process
+  (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing
+  `#11254 <https://github.com/coq/coq/pull/11254>`_).
+- **Deprecated:** The ``-quick`` command is renamed to ``-vio``, for
+  consistency with the new ``-vos`` and ``-vok`` flags. Usage of
+  ``-quick`` is now deprecated (`#11280
+  <https://github.com/coq/coq/pull/11280>`_, by Arthur Charguéraud).
+- **Fixed:**
+  ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable
+  together with an unpacked (``mllib``) plugin. (`#11357
+  <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert).
+- **Fixed:**
+  ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints
+  commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_,
+  fixes `#11353 <https://github.com/coq/coq/issues/11353>`_,
+  by Karl Palmskog).
+
+**CoqIDE**
+
+- **Changed:** CoqIDE now uses the GtkSourceView native implementation
+  of the autocomplete mechanism (`#11400
+  <https://github.com/coq/coq/pull/11400>`_, by Pierre-Marie Pédrot).
+
+**Standard library**
+
+- **Removed:** Export of module :g:`RList` in :g:`Ranalysis` and
+  :g:`Ranalysis_reg`. Module :g:`RList` is still there but must be
+  imported explicitly where required (`#11396
+  <https://github.com/coq/coq/pull/11396>`_, by Michael Soegtrop).
+
+**Infrastructure and dependencies**
+
+- **Added:**
+  Build date can now be overriden by setting the `SOURCE_DATE_EPOCH`
+  environment variable
+  (`#11227 <https://github.com/coq/coq/pull/11227>`_,
+  by Bernhard M. Wiedemann).
+
 Version 8.10
 ------------