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

Reviewed-by: cpitclaudel

5 files changed, 0 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).