Merge PR #10152: Move last changelog entries for 8.10+beta1.

Reviewed-by: vbgl

7 files changed, 58 insertions, 42 deletions

diff --git a/doc/changelog/03-notations/10061-print-custom-grammar.rst b/doc/changelog/03-notations/10061-print-custom-grammar.rst
deleted file mode 100644
index 8786c7ce6b..0000000000
--- a/doc/changelog/03-notations/10061-print-custom-grammar.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar`
-  (`#10061 <https://github.com/coq/coq/pull/10061>`_,
-  fixes `#9681 <http://github.com/coq/coq/pull/9681>`_,
-  by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin).
diff --git a/doc/changelog/04-tactics/09996-hint-mode.rst b/doc/changelog/04-tactics/09996-hint-mode.rst
deleted file mode 100644
index 06e9059b45..0000000000
--- a/doc/changelog/04-tactics/09996-hint-mode.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- Modes are now taken into account by :tacn:`typeclasses eauto` for
-  local hypotheses
-  (`#9996 <https://github.com/coq/coq/pull/9996>`_,
-  fixes `#5752 <https://github.com/coq/coq/issues/5752>`_,
-  by Maxime Dénès, review by Pierre-Marie Pédrot).
diff --git a/doc/changelog/04-tactics/10059-change-no-check.rst b/doc/changelog/04-tactics/10059-change-no-check.rst
deleted file mode 100644
index 987b2a8ccd..0000000000
--- a/doc/changelog/04-tactics/10059-change-no-check.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- New variant :tacn:`change_no_check` of :tacn:`change`, usable as a
-  documented replacement of :tacn:`convert_concl_no_check`
-  (`#10012 <https://github.com/coq/coq/pull/10012>`_,
-  `#10017 <https://github.com/coq/coq/pull/10017>`_,
-  `#10053 <https://github.com/coq/coq/pull/10053>`_, and
-  `#10059 <https://github.com/coq/coq/pull/10059>`_,
-  by Hugo Herbelin and Paolo G. Giarrusso).
diff --git a/doc/changelog/06-ssreflect/09995-notations.rst b/doc/changelog/06-ssreflect/09995-notations.rst
deleted file mode 100644
index 3dfc45242d..0000000000
--- a/doc/changelog/06-ssreflect/09995-notations.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-- `inE` now expands `y \in r x` when `r` is a `simpl_rel`.
-  New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion
-  class, simplified `predType` interface: `pred_class` and `mkPredType`
-  deprecated, `{pred T}` and `PredType` should be used instead.
-  `if c return t then ...` now expects `c` to be a variable bound in `t`.
-  New `nonPropType` interface matching types that do _not_ have sort `Prop`.
-  New `relpre R f` definition for the preimage of a relation R under f
-  (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier).
diff --git a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst
deleted file mode 100644
index 732c088f45..0000000000
--- a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull`
-  (`#9984 <https://github.com/coq/coq/pull/9984>`_,
-  by Jean-Christophe Léchenet and Oliver Nash).
diff --git a/doc/changelog/12-misc/09964-changes.rst b/doc/changelog/12-misc/09964-changes.rst
deleted file mode 100644
index dd873cfdd5..0000000000
--- a/doc/changelog/12-misc/09964-changes.rst
+++ /dev/null
@@ -1,14 +0,0 @@
-- Changelog has been moved from a specific file `CHANGES.md` to the
-  reference manual; former Credits chapter of the reference manual has
-  been split in two parts: a History chapter which was enriched with
-  additional historical information about Coq versions 1 to 5, and a
-  Changes chapter which was enriched with the content formerly in
-  `CHANGES.md` and `COMPATIBILITY`
-  (`#9133 <https://github.com/coq/coq/pull/9133>`_,
-  `#9668 <https://github.com/coq/coq/pull/9668>`_,
-  `#9939 <https://github.com/coq/coq/pull/9939>`_,
-  `#9964 <https://github.com/coq/coq/pull/9964>`_,
-  and `#10085 <https://github.com/coq/coq/pull/10085>`_,
-  by Théo Zimmermann,
-  with help and ideas from Emilio Jesús Gallego Arias, Gaëtan
-  Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 574b943a78..cca3b2e06b 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -355,6 +355,11 @@ Other changes in 8.10+beta1
     that will do it automatically, using the output of ``coqc``
     (`#8638 <https://github.com/coq/coq/pull/8638>`_, by Jason Gross).
 
+  - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar`
+    (`#10061 <https://github.com/coq/coq/pull/10061>`_,
+    fixes `#9681 <http://github.com/coq/coq/pull/9681>`_,
+    by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin).
+
 - The `quote plugin
   <https://coq.inria.fr/distrib/V8.9.0/refman/proof-engine/detailed-tactic-examples.html#quote>`_
   was removed. If some users are interested in maintaining this plugin
@@ -400,7 +405,32 @@ Other changes in 8.10+beta1
     closes `#7632 <https://github.com/coq/coq/issues/7632>`_,
     by Théo Zimmermann).
 
-  - SSReflect clear discipline made consistent across the entire proof language.
+  - Modes are now taken into account by :tacn:`typeclasses eauto` for
+    local hypotheses
+    (`#9996 <https://github.com/coq/coq/pull/9996>`_,
+    fixes `#5752 <https://github.com/coq/coq/issues/5752>`_,
+    by Maxime Dénès, review by Pierre-Marie Pédrot).
+
+  - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a
+    documented replacement of :tacn:`convert_concl_no_check`
+    (`#10012 <https://github.com/coq/coq/pull/10012>`_,
+    `#10017 <https://github.com/coq/coq/pull/10017>`_,
+    `#10053 <https://github.com/coq/coq/pull/10053>`_, and
+    `#10059 <https://github.com/coq/coq/pull/10059>`_,
+    by Hugo Herbelin and Paolo G. Giarrusso).
+
+  - The simplified value returned by :tacn:`field_simplify` is not
+    always a fraction anymore.  When the denominator is :g:`1`, it
+    returns :g:`x` while previously it was returning :g:`x/1`.  This
+    change could break codes that were post-processing application of
+    :tacn:`field_simplify` to get rid of these :g:`x/1`
+    (`#9854 <https://github.com/coq/coq/pull/9854>`_,
+    by Laurent Théry,
+    with help from Michael Soegtrop, Maxime Dénès, and Vincent Laporte).
+
+- SSReflect:
+
+  - Clear discipline made consistent across the entire proof language.
     Whenever a clear switch `{x..}` comes immediately before an existing proof
     context entry (used as a view, as a rewrite rule or as name for a new
     context entry) then such entry is cleared too.
@@ -414,6 +444,15 @@ Other changes in 8.10+beta1
 
     (`#9341 <https://github.com/coq/coq/pull/9341>`_, by Enrico Tassi).
 
+  - `inE` now expands `y \in r x` when `r` is a `simpl_rel`.
+    New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion
+    class, simplified `predType` interface: `pred_class` and `mkPredType`
+    deprecated, `{pred T}` and `PredType` should be used instead.
+    `if c return t then ...` now expects `c` to be a variable bound in `t`.
+    New `nonPropType` interface matching types that do _not_ have sort `Prop`.
+    New `relpre R f` definition for the preimage of a relation R under f
+    (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier).
+
 - Vernacular commands:
 
   - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`.
@@ -535,10 +574,28 @@ Other changes in 8.10+beta1
     `fset` database
     (`#9725 <https://github.com/coq/coq/pull/9725>`_, by Frédéric Besson).
 
+  - Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull`
+    (`#9984 <https://github.com/coq/coq/pull/9984>`_,
+    by Jean-Christophe Léchenet and Oliver Nash).
+
 - Some error messages that show problems with a pair of non-matching
   values will now highlight the differences
   (`#8669 <https://github.com/coq/coq/pull/8669>`_, by Jim Fehrle).
 
+- Changelog has been moved from a specific file `CHANGES.md` to the
+  reference manual; former Credits chapter of the reference manual has
+  been split in two parts: a History chapter which was enriched with
+  additional historical information about Coq versions 1 to 5, and a
+  Changes chapter which was enriched with the content formerly in
+  `CHANGES.md` and `COMPATIBILITY`
+  (`#9133 <https://github.com/coq/coq/pull/9133>`_,
+  `#9668 <https://github.com/coq/coq/pull/9668>`_,
+  `#9939 <https://github.com/coq/coq/pull/9939>`_,
+  `#9964 <https://github.com/coq/coq/pull/9964>`_,
+  and `#10085 <https://github.com/coq/coq/pull/10085>`_,
+  by Théo Zimmermann,
+  with help and ideas from Emilio Jesús Gallego Arias, Gaëtan
+  Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi).
 
 Version 8.9
 -----------