5 files changed, 32 insertions, 2 deletions
diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst
new file mode 100644
index 0000000000..01f2e893ed
--- /dev/null
+++ b/doc/changelog/03-notations/10180-deprecate-notations.rst
@@ -0,0 +1,6 @@
+- The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated`
+  attribute. The former `compat` annotation for notations is
+  deprecated, and its semantics changed. It is now made equivalent to using
+  a `deprecated` attribute, and is no longer connected with the `-compat`
+  command-line flag.
+  (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès).
diff --git a/doc/changelog/06-ssreflect/10302-case-HoTT.rst b/doc/changelog/06-ssreflect/10302-case-HoTT.rst
new file mode 100644
index 0000000000..686b3c3cca
--- /dev/null
+++ b/doc/changelog/06-ssreflect/10302-case-HoTT.rst
@@ -0,0 +1,7 @@
+- 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
new file mode 100644
index 0000000000..b82de1a879
--- /dev/null
+++ b/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst
@@ -0,0 +1,7 @@
+- 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/sphinx/changes.rst b/doc/sphinx/changes.rst
index db4ebd5e38..ce3e10896c 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -120,7 +120,9 @@ reference manual. Here are the most important user-visible changes:
 
 - CoqIDE:
 
-  - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2
+  - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2.
+    The INSTALL file available in the Coq sources has been updated to list
+    the new dependencies
     (`#9279 <https://github.com/coq/coq/pull/9279>`_,
     by Hugo Herbelin, with help from Jacques Garrigue,
     Emilio Jesús Gallego Arias, Michael Sogetrop and Vincent Laporte).
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index ebaa6fde66..38f6714f46 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1508,7 +1508,10 @@ the following attributes names are recognized:
     Takes as value the optional attributes ``since`` and ``note``;
     both have a string value.
 
-    This attribute can trigger the following warnings:
+    This attribute is supported by the following commands: :cmd:`Ltac`,
+    :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`.
+
+    It can trigger the following warnings:
 
     .. warn:: Tactic @qualid is deprecated since @string. @string.
        :undocumented:
@@ -1516,6 +1519,11 @@ the following attributes names are recognized:
     .. warn:: Tactic Notation @qualid is deprecated since @string. @string.
        :undocumented:
 
+    .. warn:: Notation @string__1 is deprecated since @string__2. @string__3.
+
+       :n:`@string__1` is the actual notation, :n:`@string__2` is the version number,
+       :n:`@string__3` is the note.
+
 .. example::
 
    .. coqtop:: all reset warn