Merge PR #10753: Release notes for 8.10+beta3.

Reviewed-by: cpitclaudel

6 files changed, 68 insertions, 54 deletions

diff --git a/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst b/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst
deleted file mode 100644
index 87e89a70f1..0000000000
--- a/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst
+++ /dev/null
@@ -1,30 +0,0 @@
-- Fix soundness issue with template polymorphism (`#9294
-  <https://github.com/coq/coq/issues/9294>`_)
-
-  Declarations of template-polymorphic inductive types ignored the
-  provenance of the universes they were abstracting on and did not
-  detect if they should be greater or equal to :math:`\Set` in
-  general. Previous universes and universes introduced by the inductive
-  definition could have constraints that prevented their instantiation
-  with e.g. :math:`\Prop`, resulting in unsound instantiations later. The
-  implemented fix only allows abstraction over universes introduced by
-  the inductive declaration, and properly records all their constraints
-  by making them by default only :math:`>= \Prop`. It is also checked
-  that a template polymorphic inductive actually is polymorphic on at
-  least one universe.
-
-  This prevents inductive declarations in sections to be universe
-  polymorphic over section parameters. For a backward compatible fix,
-  simply hoist the inductive definition out of the section.
-  An alternative is to declare the inductive as universe-polymorphic and
-  cumulative in a universe-polymorphic section: all universes and
-  constraints will be properly gathered in this case.
-  See :ref:`Template-polymorphism` for a detailed exposition of the
-  rules governing template-polymorphic types.
-
-  To help users incrementally fix this issue, a command line option
-  `-no-template-check` and a global flag :flag:`Template Check` are
-  available to selectively disable the new check. Use at your own risk.
-
-  (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau
-  and Maxime Dénès).
diff --git a/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst b/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst
deleted file mode 100644
index 151c400b2c..0000000000
--- a/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- Improve the ambiguous paths warning to indicate which path is ambiguous with
-  new one
-  (`#10336 <https://github.com/coq/coq/pull/10336>`_,
-  closes `#3219 <https://github.com/coq/coq/issues/3219>`_,
-  by Kazuhiko Sakaguchi).
diff --git a/doc/changelog/08-tools/10430-extraction-int63.rst b/doc/changelog/08-tools/10430-extraction-int63.rst
deleted file mode 100644
index 68ae4591a4..0000000000
--- a/doc/changelog/08-tools/10430-extraction-int63.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- Fix extraction to OCaml of primitive machine integers;
-  see :ref:`primitive-integers`
-  (`#10430 <https://github.com/coq/coq/pull/10430>`_,
-  fixes `#10361 <https://github.com/coq/coq/issues/10361>`_,
-  by Vincent Laporte).
diff --git a/doc/changelog/08-tools/10577-extraction-dependent-projections.rst b/doc/changelog/08-tools/10577-extraction-dependent-projections.rst
deleted file mode 100644
index 4d52355542..0000000000
--- a/doc/changelog/08-tools/10577-extraction-dependent-projections.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-- Fix a printing bug of OCaml extraction on dependent record projections, which
-  produced improper `assert false`. This change makes the OCaml extractor
-  internally inline record projections by default; thus the monolithic OCaml
-  extraction (:cmd:`Extraction` and :cmd:`Recursive Extraction`) does not
-  produce record projection constants anymore except for record projections
-  explicitly instructed to extract, and records declared in opaque modules
-  (`#10577 <https://github.com/coq/coq/pull/10577>`_,
-  fixes `#7348 <https://github.com/coq/coq/issues/7348>`_,
-  by Kazuhiko Sakaguchi).
diff --git a/doc/changelog/10-standard-library/09379-splitAt.rst b/doc/changelog/10-standard-library/09379-splitAt.rst
deleted file mode 100644
index 7ffe8e27f7..0000000000
--- a/doc/changelog/10-standard-library/09379-splitAt.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- Added ``splitat`` function and lemmas about ``splitat`` and ``uncons``
-  (`#9379 <https://github.com/coq/coq/pull/9379>`_,
-  by Yishuai Li, with help of Konstantinos Kallas,
-  follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_,
-  which added ``uncons`` in 8.10+beta1).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index c591a1f1de..38b3c34209 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -649,6 +649,74 @@ Many bug fixes and documentation improvements, in particular:
   (in Proof General) `#421 <https://github.com/ProofGeneral/PG/pull/421>`_,
   by Jim Fehrle).
 
+Changes in 8.10+beta3
+~~~~~~~~~~~~~~~~~~~~~
+
+**Kernel**
+
+- Fix soundness issue with template polymorphism (`#9294
+  <https://github.com/coq/coq/issues/9294>`_).
+
+  Declarations of template-polymorphic inductive types ignored the
+  provenance of the universes they were abstracting on and did not
+  detect if they should be greater or equal to :math:`\Set` in
+  general. Previous universes and universes introduced by the inductive
+  definition could have constraints that prevented their instantiation
+  with e.g. :math:`\Prop`, resulting in unsound instantiations later. The
+  implemented fix only allows abstraction over universes introduced by
+  the inductive declaration, and properly records all their constraints
+  by making them by default only :math:`>= \Prop`. It is also checked
+  that a template polymorphic inductive actually is polymorphic on at
+  least one universe.
+
+  This prevents inductive declarations in sections to be universe
+  polymorphic over section parameters. For a backward compatible fix,
+  simply hoist the inductive definition out of the section.
+  An alternative is to declare the inductive as universe-polymorphic and
+  cumulative in a universe-polymorphic section: all universes and
+  constraints will be properly gathered in this case.
+  See :ref:`Template-polymorphism` for a detailed exposition of the
+  rules governing template-polymorphic types.
+
+  To help users incrementally fix this issue, a command line option
+  `-no-template-check` and a global flag :flag:`Template Check` are
+  available to selectively disable the new check. Use at your own risk.
+
+  (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau
+  and Maxime Dénès).
+
+**User messages**
+
+- Improve the ambiguous paths warning to indicate which path is ambiguous with
+  new one
+  (`#10336 <https://github.com/coq/coq/pull/10336>`_,
+  closes `#3219 <https://github.com/coq/coq/issues/3219>`_,
+  by Kazuhiko Sakaguchi).
+
+**Extraction**
+
+- Fix extraction to OCaml of primitive machine integers;
+  see :ref:`primitive-integers`
+  (`#10430 <https://github.com/coq/coq/pull/10430>`_,
+  fixes `#10361 <https://github.com/coq/coq/issues/10361>`_,
+  by Vincent Laporte).
+- Fix a printing bug of OCaml extraction on dependent record projections, which
+  produced improper `assert false`. This change makes the OCaml extractor
+  internally inline record projections by default; thus the monolithic OCaml
+  extraction (:cmd:`Extraction` and :cmd:`Recursive Extraction`) does not
+  produce record projection constants anymore except for record projections
+  explicitly instructed to extract, and records declared in opaque modules
+  (`#10577 <https://github.com/coq/coq/pull/10577>`_,
+  fixes `#7348 <https://github.com/coq/coq/issues/7348>`_,
+  by Kazuhiko Sakaguchi).
+
+**Standard library**
+
+- Added ``splitat`` function and lemmas about ``splitat`` and ``uncons``
+  (`#9379 <https://github.com/coq/coq/pull/9379>`_,
+  by Yishuai Li, with help of Konstantinos Kallas,
+  follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_,
+  which added ``uncons`` in 8.10+beta1).
 
 Version 8.9
 -----------