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

Reviewed-by: cpitclaudel

1 files changed, 68 insertions, 0 deletions

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
 -----------