Changelog for 8.10+beta2.

5 files changed, 37 insertions, 20 deletions

diff --git a/doc/changelog/06-ssreflect/10302-case-HoTT.rst b/doc/changelog/06-ssreflect/10302-case-HoTT.rst
deleted file mode 100644
index 686b3c3cca..0000000000
--- a/doc/changelog/06-ssreflect/10302-case-HoTT.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- Make the ``case E: t`` tactic work together with
-  :flag:`Universe Polymorphism` and equality in :g:`Type`.
-  This makes tacn:`case` compatible with the HoTT
-  library https://github.com/HoTT/HoTT.
-  (`#10302 <https://github.com/coq/coq/pull/10302>`_,
-  fixes `#10301 <https://github.com/coq/coq/issues/10301>`_,
-  by Andreas Lynge, review by Enrico Tassi)
diff --git a/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst b/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst
deleted file mode 100644
index b82de1a879..0000000000
--- a/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- Make the ``rewrite /t`` tactic work together with
-  :flag:`Universe Polymorphism`.
-  This makes tacn:`rewrite` compatible with the HoTT
-  library https://github.com/HoTT/HoTT.
-  (`#10305 <https://github.com/coq/coq/pull/10305>`_,
-  fixes `#9336 <https://github.com/coq/coq/issues/9336>`_,
-  by Andreas Lynge, review by Enrico Tassi)
diff --git a/doc/changelog/09-coqide/10360-windows.rst b/doc/changelog/09-coqide/10360-windows.rst
deleted file mode 100644
index b7f8374c73..0000000000
--- a/doc/changelog/09-coqide/10360-windows.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- Fix CoqIDE instability on Windows after the update to gtk3
-  (`#10360 <https://github.com/coq/coq/pull/10360>`_, by Michael Soegtrop,
-  closes `#9885 <https://github.com/coq/coq/issues/9885>`_).
diff --git a/doc/changelog/12-misc/10019-PG-proof-diffs.rst b/doc/changelog/12-misc/10019-PG-proof-diffs.rst
deleted file mode 100644
index b2d191be26..0000000000
--- a/doc/changelog/12-misc/10019-PG-proof-diffs.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- Proof General can now display Coq-generated diffs between proof steps
-  in color.  (`#10019 <https://github.com/coq/coq/pull/10019>`_ and (in Proof General)
-  `#421 <https://github.com/ProofGeneral/PG/pull/421>`_, by Jim Fehrle).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 6ff15e52a3..e5045c222a 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -604,6 +604,43 @@ Other changes in 8.10+beta1
   with help and ideas from Emilio Jesús Gallego Arias, Gaëtan
   Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi).
 
+Changes in 8.10+beta2
+~~~~~~~~~~~~~~~~~~~~~
+
+Many bug fixes and documentation improvements, in particular:
+
+**SSReflect**
+
+- Make the ``case E: t`` tactic work together with
+  :flag:`Universe Polymorphism` and equality in :g:`Type`.
+  This makes :tacn:`case <case (ssreflect)>` compatible with the HoTT
+  library https://github.com/HoTT/HoTT
+  (`#10302 <https://github.com/coq/coq/pull/10302>`_,
+  fixes `#10301 <https://github.com/coq/coq/issues/10301>`_,
+  by Andreas Lynge, review by Enrico Tassi)
+- Make the ``rewrite /t`` tactic work together with
+  :flag:`Universe Polymorphism`.
+  This makes :tacn:`rewrite <rewrite (ssreflect)>` compatible with the HoTT
+  library https://github.com/HoTT/HoTT
+  (`#10305 <https://github.com/coq/coq/pull/10305>`_,
+  fixes `#9336 <https://github.com/coq/coq/issues/9336>`_,
+  by Andreas Lynge, review by Enrico Tassi)
+
+**CoqIDE**
+
+- Fix CoqIDE instability on Windows after the update to gtk3
+  (`#10360 <https://github.com/coq/coq/pull/10360>`_, by Michael Soegtrop,
+  closes `#9885 <https://github.com/coq/coq/issues/9885>`_).
+
+**Miscellaneous**
+
+- Proof General can now display Coq-generated diffs between proof steps
+  in color
+  (`#10019 <https://github.com/coq/coq/pull/10019>`_ and
+  (in Proof General) `#421 <https://github.com/ProofGeneral/PG/pull/421>`_,
+  by Jim Fehrle).
+
+
 Version 8.9
 -----------