Fix miscellaneous mistakes in unreleased changelog entries.

7 files changed, 12 insertions, 12 deletions

diff --git a/doc/changelog/02-specification-language/10049-bidi-app.rst b/doc/changelog/02-specification-language/10049-bidi-app.rst
index 79678c5242..279bb9272a 100644
--- a/doc/changelog/02-specification-language/10049-bidi-app.rst
+++ b/doc/changelog/02-specification-language/10049-bidi-app.rst
@@ -1,6 +1,6 @@
 - New annotation in `Arguments` for bidirectionality hints: it is now possible
   to tell type inference to use type information from the context once the `n`
   first arguments of an application are known. The syntax is:
-  `Arguments foo x y & z`.
-  `#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with
-  help from Enrico Tassi
+  `Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)`
+  (`#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with
+  help from Enrico Tassi).
diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst
index e3c3923348..2d17e569d3 100644
--- a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst
+++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst
@@ -7,6 +7,6 @@
   + notation :g:`(p | q)` now potentially clashes with core pattern syntax,
     and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`.
 
-  see :ref:`extendedpatternmatching` for details
+  See :ref:`extendedpatternmatching` for details
   (`#10167 <https://github.com/coq/coq/pull/10167>`_,
   by Georges Gonthier).
diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst
index 21ec7f8e5b..71b10aaaf4 100644
--- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst
+++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst
@@ -1,11 +1,11 @@
-- Function always opens a proof when used with a ``measure`` or ``wf``
+- :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf``
   annotation, see :ref:`advanced-recursive-functions` for the updated
   documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_,
   by Enrico Tassi).
 
-- The legacy command Add Morphism always opens a proof and cannot be used
+- The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used
   inside a module type. In order to declare a module type parameter that
-  happens to be a morphism, use ``Parameter Morphism``. See
+  happens to be a morphism, use :cmd:`Declare Morphism`. See
   :ref:`deprecated_syntax_for_generalized_rewriting` for the updated
   documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_,
   by Enrico Tassi).
diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst
index 01f2e893ed..bce5db5865 100644
--- a/doc/changelog/03-notations/10180-deprecate-notations.rst
+++ b/doc/changelog/03-notations/10180-deprecate-notations.rst
@@ -2,5 +2,5 @@
   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.
+  command-line flag
   (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès).
diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst
index 6a74551f06..0cb669778c 100644
--- a/doc/changelog/04-tactics/09288-injection-as.rst
+++ b/doc/changelog/04-tactics/09288-injection-as.rst
@@ -1,4 +1,4 @@
 - Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as
   an alternative to :n:`injection @term as {+ @simple_intropattern}` using
-  the standard :n:`@injection_intropattern` syntax (`#09288
-  <https://github.com/coq/coq/pull/09288>`_, by Hugo Herbelin).
+  the standard :n:`@injection_intropattern` syntax (`#9288
+  <https://github.com/coq/coq/pull/9288>`_, by Hugo Herbelin).
diff --git a/doc/changelog/04-tactics/10318-select-only-error.rst b/doc/changelog/04-tactics/10318-select-only-error.rst
index 03ed15d948..b4f991316e 100644
--- a/doc/changelog/04-tactics/10318-select-only-error.rst
+++ b/doc/changelog/04-tactics/10318-select-only-error.rst
@@ -1,4 +1,4 @@
 - The goal selector tactical ``only`` now checks that the goal range
   it is given is valid instead of ignoring goals out of the focus
-  range. (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan
+  range (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan
   Gilbert).
diff --git a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst
index 78874cadb1..1c91800c65 100644
--- a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst
+++ b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst
@@ -1,5 +1,5 @@
 - Deprecated flag `Refine Instance Mode` has been removed.
-  (`#09530 <https://github.com/coq/coq/pull/09530>`_, fixes
+  (`#9530 <https://github.com/coq/coq/pull/9530>`_, fixes
   `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890
   <https://github.com/coq/coq/issues/3890>`_ and `#4638
   <https://github.com/coq/coq/issues/4638>`_