Minor improvements to the unreleased changelog.

29 files changed, 41 insertions, 35 deletions

diff --git a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst
index 32526babdb..633bb6731e 100644
--- a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst
+++ b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst
@@ -1,8 +1,8 @@
 - **Added:**
   :cmd:`Arguments <Arguments (implicits)>` now supports setting
-  implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`.
+  implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`
   (`#11098 <https://github.com/coq/coq/pull/11098>`_,
   by Hugo Herbelin, fixes `#4696
   <https://github.com/coq/coq/pull/4696>`_, `#5173
   <https://github.com/coq/coq/pull/5173>`_, `#9098
-  <https://github.com/coq/coq/pull/9098>`_.).
+  <https://github.com/coq/coq/pull/9098>`_).
diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst
index a7ffde31fc..b0e658998b 100644
--- a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst
+++ b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst
@@ -1,6 +1,6 @@
 - **Changed:**
   The warning raised when a trailing implicit is declared to be non maximally
-  inserted (with the command cmd:`Arguments <Arguments (implicits)>`) has been turned into an error.
-  This was deprecated since Coq 8.10.
+  inserted (with the command :cmd:`Arguments <Arguments (implicits)>`) has been turned into an error.
+  This was deprecated since Coq 8.10
   (`#11368 <https://github.com/coq/coq/pull/11368>`_,
   by SimonBoulier).
diff --git a/doc/changelog/02-specification-language/11600-uniform-syntax.rst b/doc/changelog/02-specification-language/11600-uniform-syntax.rst
index 3fa3f80301..b95bad2eb8 100644
--- a/doc/changelog/02-specification-language/11600-uniform-syntax.rst
+++ b/doc/changelog/02-specification-language/11600-uniform-syntax.rst
@@ -1,4 +1,5 @@
 - **Added:**
   New syntax :g:`Inductive Acc A R | x : Prop := ...` to specify which
   parameters of an inductive are uniform.
+  See :ref:`parametrized-inductive-types`
   (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst
index 5393fb3d8c..a8d4fc6ed2 100644
--- a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst
+++ b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst
@@ -1 +1,6 @@
-- Different interpretations in different scopes of the same notation string can now be associated to different printing formats; this fixes bug #6092 and #7766 (`#10832 <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin).
+- **Fixed:**
+  Different interpretations in different scopes of the same notation
+  string can now be associated to different printing formats (`#10832
+  <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin,
+  fixes `#6092 <https://github.com/coq/coq/issues/6092>`_
+  and `#7766 <https://github.com/coq/coq/issues/7766>`_).
diff --git a/doc/changelog/03-notations/11650-parensNew.rst b/doc/changelog/03-notations/11650-parensNew.rst
index 5e2da594c6..f52a720428 100644
--- a/doc/changelog/03-notations/11650-parensNew.rst
+++ b/doc/changelog/03-notations/11650-parensNew.rst
@@ -1,4 +1,4 @@
 - **Added:**
-  added option Set Printing Parentheses to print parentheses even when implied by associativity or precedence.
+  added the :flag:`Printing Parentheses` flag to print parentheses even when implied by associativity or precedence.
   (`#11650 <https://github.com/coq/coq/pull/11650>`_,
   by Hugo Herbelin and Abhishek Anand).
diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst
index eeae2ec519..32cd9b7135 100644
--- a/doc/changelog/04-tactics/10760-more-rapply.rst
+++ b/doc/changelog/04-tactics/10760-more-rapply.rst
@@ -4,5 +4,5 @@
   rare cases where users were relying on :tacn:`rapply` inserting
   exactly 15 underscores and no more, due to the lemma having a
   completely unspecified codomain (and thus allowing for any number of
-  underscores), the tactic will now instead loop. (`#10760
-  <https://github.com/coq/coq/pull/10760>`_, by Jason Gross)
+  underscores), the tactic will now instead loop (`#10760
+  <https://github.com/coq/coq/pull/10760>`_, by Jason Gross).
diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst
index c72d085687..ba4d10590f 100644
--- a/doc/changelog/04-tactics/10998-zify-complements.rst
+++ b/doc/changelog/04-tactics/10998-zify-complements.rst
@@ -4,5 +4,5 @@
   `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, and `Z.quot2`.
   Injections for internal definitions in module `ZifyBool` (`isZero` and `isLeZero`)
   are also added to help users to declare new :tacn:`zify` class instances using
-  Micromega tactics.
+  Micromega tactics
   (`#10998 <https://github.com/coq/coq/pull/10998>`_, by Kazuhiko Sakaguchi).
diff --git a/doc/changelog/04-tactics/11023-nativecompute-timing.rst b/doc/changelog/04-tactics/11023-nativecompute-timing.rst
index 2afa3990ac..e8cdfcca21 100644
--- a/doc/changelog/04-tactics/11023-nativecompute-timing.rst
+++ b/doc/changelog/04-tactics/11023-nativecompute-timing.rst
@@ -3,5 +3,5 @@
   compiler) to emit separate timing information about compilation,
   execution, and reification.  It replaces the timing information
   previously emitted when the `-debug` flag was set, and allows more
-  fine-grained timing of the native compiler.  (`#11023
+  fine-grained timing of the native compiler (`#11023
   <https://github.com/coq/coq/pull/11023>`_, by Jason Gross).
diff --git a/doc/changelog/04-tactics/11288-omega+depr.rst b/doc/changelog/04-tactics/11288-omega+depr.rst
index 2832e6db61..3a2d421967 100644
--- a/doc/changelog/04-tactics/11288-omega+depr.rst
+++ b/doc/changelog/04-tactics/11288-omega+depr.rst
@@ -1,6 +1,6 @@
 - **Removed:**
   The undocumented ``omega with`` tactic variant has been removed,
-  using ``lia`` is the recommended replacement, tho the old semantics
-  of ``omega with *`` can be recovered with ``zify; omega``
+  using :tacn:`lia` is the recommended replacement, although the old semantics
+  of ``omega with *`` can also be recovered with ``zify; omega``
   (`#11288 <https://github.com/coq/coq/pull/11288>`_,
   by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst
index 5ecd46bced..79879c78d5 100644
--- a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst
+++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst
@@ -1,5 +1,5 @@
 - **Fixed:**
-  Regression of ``lia`` due to more powerful ``zify``
+  Regression of :tacn:`lia` due to more powerful :tacn:`zify`
   (`#11362 <https://github.com/coq/coq/pull/11362>`_,
   fixes `#11191 <https://github.com/coq/coq/issues/11191>`_,
   by Frédéric Besson).
diff --git a/doc/changelog/04-tactics/11370-zify-elim-let.rst b/doc/changelog/04-tactics/11370-zify-elim-let.rst
index 4eb2732106..944dde99b8 100644
--- a/doc/changelog/04-tactics/11370-zify-elim-let.rst
+++ b/doc/changelog/04-tactics/11370-zify-elim-let.rst
@@ -1,3 +1,3 @@
-- **Changed**
-  Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml.
+- **Changed:**
+  Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml
   (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson).
diff --git a/doc/changelog/04-tactics/11429-zify-optimisation.rst b/doc/changelog/04-tactics/11429-zify-optimisation.rst
index ce5bfa4aad..25927f9182 100644
--- a/doc/changelog/04-tactics/11429-zify-optimisation.rst
+++ b/doc/changelog/04-tactics/11429-zify-optimisation.rst
@@ -1,3 +1,3 @@
-- **Changed**
-  Improve the efficiency of `zify` by rewritting the remaining Ltac code in OCaml.
+- **Changed:**
+  Improve the efficiency of :tacn:`zify` by rewritting the remaining Ltac code in OCaml
   (`#11429 <https://github.com/coq/coq/pull/11429>`_, by Frédéric Besson).
diff --git a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst
index 2a341261e5..52a2b2f0f6 100644
--- a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst
+++ b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst
@@ -1,9 +1,9 @@
 - **Added:**
-  :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls.
+  :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls
   (`#11474 <https://github.com/coq/coq/pull/11474>`_,  by Frédéric Besson).
 
 - **Fixed:**
-  Efficiency regression of ``lia``
+  Efficiency regression of :tacn:`lia`
   (`#11474 <https://github.com/coq/coq/pull/11474>`_,
   fixes `#11436 <https://github.com/coq/coq/issues/11436>`_,
   by Frédéric Besson).
diff --git a/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst b/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst
index 4acc423d10..e8233b9d13 100644
--- a/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst
+++ b/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst
@@ -1,4 +1,4 @@
 - **Added:**
-  An array library for ltac2 (OCaml standard library compatible where possible).
+  An array library for Ltac2 (as compatible as possible with OCaml standard library)
   (`#10343 <https://github.com/coq/coq/pull/10343>`_,
   by Michael Soegtrop).
diff --git a/doc/changelog/05-tactic-language/11740-ltac2-enough.rst b/doc/changelog/05-tactic-language/11740-ltac2-enough.rst
index ced3e0ab60..5d3671bce1 100644
--- a/doc/changelog/05-tactic-language/11740-ltac2-enough.rst
+++ b/doc/changelog/05-tactic-language/11740-ltac2-enough.rst
@@ -1,4 +1,4 @@
 - **Added:**
-  Ltac2 notations for enough an eenough
+  Ltac2 notations for :tacn:`enough` and :tacn:`eenough`
   (`#11740 <https://github.com/coq/coq/pull/11740>`_,
   by Michael Soegtrop).
diff --git a/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst b/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst
index d2af6a4ca7..b627fdbcc9 100644
--- a/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst
+++ b/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst
@@ -1,5 +1,5 @@
 - **Deprecated:**
   Deprecated the declaration of arbitrary terms as hints. Global
-  references are now mandatory.
+  references are now preferred
   (`#7791 <https://github.com/coq/coq/pull/7791>`_,
   by Pierre-Marie Pédrot).
diff --git a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst
index e73be9c642..b263de017b 100644
--- a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst
+++ b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst
@@ -1,5 +1,5 @@
 - **Changed:**
-  The :cmd:`Print Canonical Projections` command now can take constants and
+  The :cmd:`Print Canonical Projections` command can now take constants and
   prints only the unification rules that involve or are synthesized from given
   constants (`#10747 <https://github.com/coq/coq/pull/10747>`_,
   by Kazuhiko Sakaguchi).
diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst
index ec34c075ae..2bdc8052c6 100644
--- a/doc/changelog/07-commands-and-options/11164-let-cs.rst
+++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst
@@ -1,3 +1,3 @@
-- **Added:** A section variable introduces with :g:`Let` can be
-  declared as a :g:`Canonical Structure` (`#11164
+- **Added:** A section variable introduced with :cmd:`Let` can be
+  declared as a :cmd:`Canonical Structure` (`#11164
   <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi).
diff --git a/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst b/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst
index 77fa556321..99f2d22d11 100644
--- a/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst
+++ b/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst
@@ -1,9 +1,9 @@
-- **Changed:**
+- **Removed:**
   Recursive OCaml loadpaths are not supported anymore; the command
   ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the
   preferred one. We have also dropped support for the non-qualified
   version of the :cmd:`Add LoadPath` command, that is to say,
   the ``Add LoadPath dir`` version; now,
-  you must always specify a prefix now using ``Add Loadpath dir as Prefix.``
+  you must always specify a prefix now using ``Add Loadpath dir as Prefix``
   (`#11618 <https://github.com/coq/coq/pull/11618>`_,
   by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst b/doc/changelog/08-tools/11409-mltop+deprecate_use.rst
index db433ad64c..f4f110ed67 100644
--- a/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst
+++ b/doc/changelog/08-tools/11409-mltop+deprecate_use.rst
@@ -1,5 +1,5 @@
 - **Removed:**
   The `-load-ml-source` and `-load-ml-object` command line options
   have been removed; their use was very limited, you can achieve the same adding
-  additional object files in the linking step or using a plugin.
+  additional object files in the linking step or using a plugin
   (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/08-tools/11523-coqdep+refactor2.rst b/doc/changelog/08-tools/11523-coqdep+refactor2.rst
index 32a4750b73..3f93d60926 100644
--- a/doc/changelog/08-tools/11523-coqdep+refactor2.rst
+++ b/doc/changelog/08-tools/11523-coqdep+refactor2.rst
@@ -4,7 +4,7 @@
   files are not supported as input. Also, several deprecated options
   have been removed: ``-w``, ``-D``, ``-mldep``, ``-prefix``,
   ``-slash``, and ``-dumpbox``. Passing ``-boot`` to ``coqdep`` will
-  not load any path by default now, ``-R/-Q`` should be used instead.
+  not load any path by default now, ``-R/-Q`` should be used instead
   (`#11523 <https://github.com/coq/coq/pull/11523>`_ and
   `#11589 <https://github.com/coq/coq/pull/11589>`_,
   by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst b/doc/changelog/08-tools/11617-toplevel+boot.rst
index 49dd0ee2d8..49dd0ee2d8 100644
--- a/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst
+++ b/doc/changelog/08-tools/11617-toplevel+boot.rst
diff --git a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst
index 6294cdb24a..49ac16eee9 100644
--- a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst
+++ b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst
@@ -1,4 +1,4 @@
 - **Removed:**
-  Removed the "Tactic" menu from CoqIDE which had been unmaintained for a number of years
+  "Tactic" menu from CoqIDE which had been unmaintained for a number of years
   (`#11414 <https://github.com/coq/coq/pull/11414>`_,
   by Pierre-Marie Pédrot).
diff --git a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst
index cb92945b8b..9d22a858f1 100644
--- a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst
+++ b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst
@@ -1,4 +1,4 @@
 - **Removed:**
-  Removed the "Revert all buffers" command from CoqIDE which had been broken for a long time
+  "Revert all buffers" command from CoqIDE which had been broken for a long time
   (`#11415 <https://github.com/coq/coq/pull/11415>`_,
   by Pierre-Marie Pédrot).
diff --git a/doc/changelog/10-standard-library/11127-trunk.rst b/doc/changelog/10-standard-library/11127-trunk.rst
index ef1d41d17f..3f461397ae 100644
--- a/doc/changelog/10-standard-library/11127-trunk.rst
+++ b/doc/changelog/10-standard-library/11127-trunk.rst
@@ -1,2 +1,2 @@
-- **Added:** theorem :g:`bezout_comm` for natural numbers
+- **Added:** Theorem :g:`bezout_comm` for natural numbers
   (`#11127 <https://github.com/coq/coq/pull/11127>`_, by Daniel de Rauglaudre).
diff --git a/doc/changelog/03-notations/11240-rew-dependent.rst b/doc/changelog/10-standard-library/11240-rew-dependent.rst
index e9daab0c2c..e9daab0c2c 100644
--- a/doc/changelog/03-notations/11240-rew-dependent.rst
+++ b/doc/changelog/10-standard-library/11240-rew-dependent.rst
diff --git a/doc/changelog/10-standard-library/11686-fix-int-notations.rst b/doc/changelog/10-standard-library/11686-fix-int-notations.rst
index cc820c5a25..4959a9f9b1 100644
--- a/doc/changelog/10-standard-library/11686-fix-int-notations.rst
+++ b/doc/changelog/10-standard-library/11686-fix-int-notations.rst
@@ -2,5 +2,5 @@
   Notations :n:`[|@term|]` and :n:`[||@term||]` for morphisms from 63-bit
   integers to :g:`Z` and :g:`zn2z int` have been removed in favor of
   :n:`φ(@term)` and :n:`Φ(@term)` respectively. These notations were
-  breaking Ltac parsing. (`#11686 <https://github.com/coq/coq/pull/11686>`_,
+  breaking Ltac parsing (`#11686 <https://github.com/coq/coq/pull/11686>`_,
   by Maxime Dénès).
diff --git a/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst b/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst
index 03c2ccc1d2..dc76178e0d 100644
--- a/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst
+++ b/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst
@@ -1,4 +1,4 @@
 - **Removed:**
-  Python 2 is not longer required in any part of the codebase.
+  Python 2 is not longer required in any part of the codebase
   (`#11245 <https://github.com/coq/coq/pull/11245>`_,
   by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/12-misc/10486-native-string-extraction.rst b/doc/changelog/12-misc/10486-native-string-extraction.rst
index c6778403d4..0636e303c4 100644
--- a/doc/changelog/12-misc/10486-native-string-extraction.rst
+++ b/doc/changelog/12-misc/10486-native-string-extraction.rst
@@ -2,6 +2,6 @@
   Support for better extraction of strings in OCaml and Haskell:
   `ExtOcamlNativeString` provides bindings from the Coq `String` type to
   the OCaml `string` type, and string literals can be extracted to literals,
-  both in OCaml and Haskell. (`#10486
+  both in OCaml and Haskell (`#10486
   <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from
   Maxime Dénès, review by Hugo Herbelin).