Merge PR #10931: Add types of changes to changelog entries.

Ack-by: SkySkimmer
Reviewed-by: ejgallego

52 files changed, 177 insertions, 96 deletions

diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh
index dbb60359cb..e1aed4560d 100755
--- a/dev/tools/make-changelog.sh
+++ b/dev/tools/make-changelog.sh
@@ -3,7 +3,7 @@
 printf "PR number? "
 read -r PR
 
-printf "Where? (type a prefix)\n"
+printf "Category? (type a prefix)\n"
 (cd doc/changelog && ls -d */)
 read -r where
 
@@ -11,11 +11,25 @@ where="doc/changelog/$where"
 if ! [ -d "$where" ]; then where=$(echo "$where"*); fi
 where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst"
 
+printf "Type? (type first letter)\n"
+printf "[A]dded \t[C]hanged \t[D]eprecated \t[F]ixed \t[R]emoved\n"
+read -r type_first_letter
+
+case "$type_first_letter" in
+  [Aa]) type_full="Added";;
+  [Cc]) type_full="Changed";;
+  [Dd]) type_full="Deprecated";;
+  [Ff]) type_full="Fixed";;
+  [Rr]) type_full="Removed";;
+  *) printf "Invalid input!\n"
+     exit 1;;
+esac
+
 # shellcheck disable=SC2016
 # the ` are regular strings, this is intended
 # use %s for the leading - to avoid looking like an option (not sure
 # if necessary but doesn't hurt)
-printf '%s bla bla (`#%s <https://github.com/coq/coq/pull/%s>`_, by %s).' - "$PR" "$PR" "$(git config user.name)" > "$where"
+printf '%s **%s:**\n  Bla bla\n  (`#%s <https://github.com/coq/coq/pull/%s>`_,\n  by %s).' - "$type_full" "$PR" "$PR" "$(git config user.name)" > "$where"
 
 printf "Name of created changelog file:\n"
 printf "$where\n"
diff --git a/doc/changelog/01-kernel/09867-floats.rst b/doc/changelog/01-kernel/09867-floats.rst
index 56b5fc747a..cae4dbb335 100644
--- a/doc/changelog/01-kernel/09867-floats.rst
+++ b/doc/changelog/01-kernel/09867-floats.rst
@@ -1,4 +1,5 @@
-- A built-in support of floating-point arithmetic was added, allowing
+- **Added:**
+  A built-in support of floating-point arithmetic, allowing
   one to devise efficient reflection tactics involving numerical
   computation. Primitive floats are added in the language of terms,
   following the binary64 format of the IEEE 754 standard, and the
diff --git a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md
deleted file mode 100644
index e0573a2c74..0000000000
--- a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md
+++ /dev/null
@@ -1,4 +0,0 @@
-- Internal definitions generated by abstract-like tactics are now inlined
-  inside universe Qed-terminated polymorphic definitions, similarly to what
-  happens for their monomorphic counterparts,
-  (`#10439 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot).
diff --git a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst
new file mode 100644
index 0000000000..84060ddf29
--- /dev/null
+++ b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Internal definitions generated by :tacn:`abstract`\-like tactics are now inlined
+  inside universe :cmd:`Qed`\-terminated polymorphic definitions, similarly to what
+  happens for their monomorphic counterparts,
+  (`#10439 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot).
diff --git a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst
index bac08d12ea..5d224797d4 100644
--- a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst
+++ b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst
@@ -1,6 +1,7 @@
-- Section data is now part of the kernel. Solves a soundness issue
+- **Fixed:**
+  Section data is now part of the kernel. Solves a soundness issue
   in interactive mode where global monomorphic universe constraints would be
   dropped when forcing a delayed opaque proof inside a polymorphic section. Also
   relaxes the nesting criterion for sections, as polymorphic sections can now
   appear inside a monomorphic one
-  (#10664, <https://github.com/coq/coq/pull/10664> by Pierre-Marie Pédrot).
+  (`#10664, <https://github.com/coq/coq/pull/10664>`_ by Pierre-Marie Pédrot).
diff --git a/doc/changelog/01-kernel/10811-sprop-default-on.rst b/doc/changelog/01-kernel/10811-sprop-default-on.rst
index 349c44c205..2c008fb5d3 100644
--- a/doc/changelog/01-kernel/10811-sprop-default-on.rst
+++ b/doc/changelog/01-kernel/10811-sprop-default-on.rst
@@ -1,3 +1,4 @@
-- Using ``SProp`` is now allowed by default, without needing to pass
+- **Changed:**
+  Using ``SProp`` is now allowed by default, without needing to pass
   ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811
   <https://github.com/coq/coq/pull/10811>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/02-specification-language/10049-bidi-app.rst b/doc/changelog/02-specification-language/10049-bidi-app.rst
index 279bb9272a..024795f5da 100644
--- a/doc/changelog/02-specification-language/10049-bidi-app.rst
+++ b/doc/changelog/02-specification-language/10049-bidi-app.rst
@@ -1,4 +1,5 @@
-- New annotation in `Arguments` for bidirectionality hints: it is now possible
+- **Added:**
+  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`. See :cmd:`Arguments (bidirectionality hints)`
diff --git a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
index 0a902079b9..389ee4fd7f 100644
--- a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
+++ b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
@@ -1,4 +1,5 @@
-- Record fields can be annotated to prevent them from being used as canonical projections;
+- **Added:**
+  Record fields can be annotated to prevent them from being used as canonical projections;
   see :ref:`canonicalstructures` for details
   (`#10076 <https://github.com/coq/coq/pull/10076>`_,
   by Vincent Laporte).
diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst
index 2d17e569d3..87e4c9ff10 100644
--- a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst
+++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst
@@ -1,11 +1,14 @@
-- Require parentheses around nested disjunctive patterns, so that pattern and
+- **Changed:**
+  Require parentheses around nested disjunctive patterns, so that pattern and
   term syntax are consistent; match branch patterns no longer require
-  parentheses for notation at level 100 or more. Incompatibilities:
+  parentheses for notation at level 100 or more.
 
-  + in :g:`match p with (_, (0|1)) => ...` parentheses may no longer be
-    omitted around :n:`0|1`.
-  + notation :g:`(p | q)` now potentially clashes with core pattern syntax,
-    and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`.
+  .. warning:: Incompatibilities
+
+     + In :g:`match p with (_, (0|1)) => ...` parentheses may no longer be
+       omitted around :n:`0|1`.
+     + 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
   (`#10167 <https://github.com/coq/coq/pull/10167>`_,
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 71b10aaaf4..c201b482e5 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,9 +1,11 @@
-- :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf``
+- **Changed:**
+  :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 :cmd:`Add Morphism` always opens a proof and cannot be used
+- **Changed:**
+  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 :cmd:`Declare Morphism`. See
   :ref:`deprecated_syntax_for_generalized_rewriting` for the updated
diff --git a/doc/changelog/02-specification-language/10441-static-poly-section.rst b/doc/changelog/02-specification-language/10441-static-poly-section.rst
index 7f0345d946..3d0ca000e6 100644
--- a/doc/changelog/02-specification-language/10441-static-poly-section.rst
+++ b/doc/changelog/02-specification-language/10441-static-poly-section.rst
@@ -1,11 +1,13 @@
-- The universe polymorphism setting now applies from the opening of a section.
+- **Changed:**
+  The universe polymorphism setting now applies from the opening of a section.
   In particular, it is not possible anymore to mix polymorphic and monomorphic
   definitions in a section when there are no variables nor universe constraints
   defined in this section. This makes the behaviour consistent with the
   documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_,
   by Pierre-Marie Pédrot)
 
-- The :cmd:`Section` vernacular command now accepts the "universes" attribute. In
+- **Added:**
+  The :cmd:`Section` vernacular command now accepts the "universes" attribute. In
   addition to setting the section universe polymorphism, it also locally sets
   the universe polymorphic option inside the section.
   (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot)
diff --git a/doc/changelog/02-specification-language/10758-fix-10757.rst b/doc/changelog/02-specification-language/10758-fix-10757.rst
index 4cce26aedc..431123ec1b 100644
--- a/doc/changelog/02-specification-language/10758-fix-10757.rst
+++ b/doc/changelog/02-specification-language/10758-fix-10757.rst
@@ -1,4 +1,5 @@
-- ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes
+- **Fixed:**
+  ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes
   involving ``Prop`` types (`#10758
   <https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing
   `#10757 <https://github.com/coq/coq/issues/10757>`_ reported by
diff --git a/doc/changelog/02-specification-language/10985-about-arguments.rst b/doc/changelog/02-specification-language/10985-about-arguments.rst
index 1e05b0b0fe..0faaf95e6c 100644
--- a/doc/changelog/02-specification-language/10985-about-arguments.rst
+++ b/doc/changelog/02-specification-language/10985-about-arguments.rst
@@ -1,5 +1,6 @@
-- The output of the :cmd:`Print` and :cmd:`About` commands has
-  changed. Arguments meta-data is now displayed as the corresponding
+- **Changed:**
+  Output of the :cmd:`Print` and :cmd:`About` commands.
+  Arguments meta-data is now displayed as the corresponding
   :cmd:`Arguments <Arguments (implicits)>` command instead of the
   human-targeted prose used in previous Coq versions. (`#10985
   <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst
index cd1a692f54..51a62a0c8d 100644
--- a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst
+++ b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst
@@ -1,4 +1,4 @@
-- Added ``#[refine]`` attribute for :cmd:`Instance`, a more
+- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more
   predictable version of the old ``Refine Instance Mode`` which
   unconditionally opens a proof (`#10996
   <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst
index 43a748b365..49f8f451a7 100644
--- a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst
+++ b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst
@@ -1,3 +1,4 @@
-- The unsupported attribute error is now an error-by-default warning,
+- **Changed:**
+  The unsupported attribute error is now an error-by-default warning,
   meaning it can be disabled (`#10997
   <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst
index f8298cdbdd..6bf261eb9b 100644
--- a/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst
+++ b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst
@@ -1,4 +1,4 @@
-- Fixed bugs sometimes preventing to define valid (co)fixpoints with implicit arguments
+- **Fixed:** Bugs sometimes preventing to define valid (co)fixpoints with implicit arguments
   in the presence of local definitions, see `#3282 <https://github.com/coq/coq/issues/3282>`_
   (`#11132 <https://github.com/coq/coq/pull/11132>`_, by Hugo Herbelin).
 
diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst
index abc5a516ae..ed95a6eb4f 100644
--- a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst
+++ b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst
@@ -1,4 +1,5 @@
-- Numeral Notations now support sorts in the input to printing
+- **Added:**
+  Numeral Notations now support sorts in the input to printing
   functions (e.g., numeral notations can be defined for terms
   containing things like `@cons Set nat nil`).  (`#9883
   <https://github.com/coq/coq/pull/9883>`_, by Jason Gross).
diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst
index bce5db5865..a3c185d5f1 100644
--- a/doc/changelog/03-notations/10180-deprecate-notations.rst
+++ b/doc/changelog/03-notations/10180-deprecate-notations.rst
@@ -1,5 +1,10 @@
-- The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated`
-  attribute. The former `compat` annotation for notations is
+- **Added:**
+  The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated`
+  attribute
+  (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès).
+
+- **Deprecated:**
+  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
diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst
index 327a39bdb6..5dc0215225 100644
--- a/doc/changelog/03-notations/10963-simplify-parser.rst
+++ b/doc/changelog/03-notations/10963-simplify-parser.rst
@@ -1,4 +1,5 @@
-- A simplification of parsing rules could cause a slight change of
+- **Changed:**
+  A simplification of parsing rules could cause a slight change of
   parsing precedences for the very rare users who defined notations
   with `constr` at level strictly between 100 and 200 and used these
   notations on the right-hand side of a cast operator (`:`, `:>`,
diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst
index 0cb669778c..0efae6902f 100644
--- a/doc/changelog/04-tactics/09288-injection-as.rst
+++ b/doc/changelog/04-tactics/09288-injection-as.rst
@@ -1,4 +1,5 @@
-- Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as
+- **Added:**
+  Syntax :n:`injection @term as [= {+ @intropattern} ]` as
   an alternative to :n:`injection @term as {+ @simple_intropattern}` using
   the standard :n:`@injection_intropattern` syntax (`#9288
   <https://github.com/coq/coq/pull/9288>`_, by Hugo Herbelin).
diff --git a/doc/changelog/04-tactics/09856-zify.rst b/doc/changelog/04-tactics/09856-zify.rst
index 6b9143c77b..c71a715ccc 100644
--- a/doc/changelog/04-tactics/09856-zify.rst
+++ b/doc/changelog/04-tactics/09856-zify.rst
@@ -1,6 +1,7 @@
-- Reimplementation of the :tacn:`zify` tactic. The tactic is more efficient and copes with dependent hypotheses.
+- **Changed:**
+  Reimplementation of the :tacn:`zify` tactic. The tactic is more efficient and copes with dependent hypotheses.
   It can also be extended by redefining the tactic ``zify_post_hook``.
-  (`#9856 <https://github.com/coq/coq/pull/9856>`_ fixes
+  (`#9856 <https://github.com/coq/coq/pull/9856>`_, fixes
   `#8898 <https://github.com/coq/coq/issues/8898>`_,
   `#7886 <https://github.com/coq/coq/issues/7886>`_,
   `#9848 <https://github.com/coq/coq/issues/9848>`_ and
diff --git a/doc/changelog/04-tactics/10318-select-only-error.rst b/doc/changelog/04-tactics/10318-select-only-error.rst
index b4f991316e..3e4874dee6 100644
--- a/doc/changelog/04-tactics/10318-select-only-error.rst
+++ b/doc/changelog/04-tactics/10318-select-only-error.rst
@@ -1,4 +1,5 @@
-- The goal selector tactical ``only`` now checks that the goal range
+- **Changed:**
+  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
   Gilbert).
diff --git a/doc/changelog/04-tactics/10765-micromega-caches.rst b/doc/changelog/04-tactics/10765-micromega-caches.rst
index 12d8f68e63..82c14bcfdd 100644
--- a/doc/changelog/04-tactics/10765-micromega-caches.rst
+++ b/doc/changelog/04-tactics/10765-micromega-caches.rst
@@ -1,3 +1,4 @@
-- Introduction of flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`.
-  (see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case)
-  (`#10765 <https://github.com/coq/coq/pull/10765>`_ fixes `#10772 <https://github.com/coq/coq/issues/10772>`_ , by Frédéric Besson).
+- **Added:**
+  Flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`.
+  (`#10765 <https://github.com/coq/coq/pull/10765>`_, by Frédéric Besson,
+  see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case).
diff --git a/doc/changelog/04-tactics/10774-zify-Z_to_N.rst b/doc/changelog/04-tactics/10774-zify-Z_to_N.rst
index ed46cb101e..37a47a3c98 100644
--- a/doc/changelog/04-tactics/10774-zify-Z_to_N.rst
+++ b/doc/changelog/04-tactics/10774-zify-Z_to_N.rst
@@ -1,3 +1,4 @@
-- The :tacn:`zify` tactic is now aware of `Z.to_N`.
-  (`#10774 <https://github.com/coq/coq/pull/10774>`_ fixes
+- **Added:**
+  The :tacn:`zify` tactic is now aware of `Z.to_N`.
+  (`#10774 <https://github.com/coq/coq/pull/10774>`_, grants
   `#9162 <https://github.com/coq/coq/issues/9162>`_, by Kazuhiko Sakaguchi).
diff --git a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst
index 09bef82c80..755febc39d 100644
--- a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst
+++ b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst
@@ -1,11 +1,13 @@
-- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now
+- **Changed:**
+  The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now
   only run their tactic argument once, even if it has multiple
   successes.  This prevents blow-up and looping from using
   multisuccess tactics with :tacn:`assert_succeeds`.  (`#10966
   <https://github.com/coq/coq/pull/10966>`_ fixes `#10965
   <https://github.com/coq/coq/issues/10965>`_, by Jason Gross).
 
-- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now
+- **Fixed:**
+  The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now
   behave correctly when their tactic fully solves the goal.  (`#10966
   <https://github.com/coq/coq/pull/10966>`_ fixes `#9114
   <https://github.com/coq/coq/issues/9114>`_, by Jason Gross).
diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst
index 3ec526f0a9..c72d085687 100644
--- a/doc/changelog/04-tactics/10998-zify-complements.rst
+++ b/doc/changelog/04-tactics/10998-zify-complements.rst
@@ -1,4 +1,5 @@
-- The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`,
+- **Added:**
+  The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`,
   `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`,
   `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, and `Z.quot2`.
   Injections for internal definitions in module `ZifyBool` (`isZero` and `isLeZero`)
diff --git a/doc/changelog/05-tactic-language/10002-ltac2.rst b/doc/changelog/05-tactic-language/10002-ltac2.rst
index 6d62f11eff..8b910a4779 100644
--- a/doc/changelog/05-tactic-language/10002-ltac2.rst
+++ b/doc/changelog/05-tactic-language/10002-ltac2.rst
@@ -1,4 +1,5 @@
-- Ltac2, a new version of the tactic language Ltac, that doesn't
+- **Added:**
+  Ltac2, a new version of the tactic language Ltac, that doesn't
   preserve backward compatibility, has been integrated in the main Coq
   distribution.  It is still experimental, but we already recommend
   users of advanced Ltac to start using it and report bugs or request
diff --git a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst
index bd1c0c42e8..f32443cbb9 100644
--- a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst
+++ b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst
@@ -1,4 +1,5 @@
-- Ltac2 tactic notations with “constr” arguments can specify the
+- **Added:**
+  Ltac2 tactic notations with “constr” arguments can specify the
   interpretation scope for these arguments;
   see :ref:`ltac2_notations` for details
   (`#10289 <https://github.com/coq/coq/pull/10289>`_,
diff --git a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst
index fba09f5e87..16ca9caf48 100644
--- a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst
+++ b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst
@@ -1,4 +1,5 @@
-- White spaces are forbidden in the “&ident” syntax for ltac2 references
+- **Changed:**
+  White spaces are forbidden in the :n:`&@ident` syntax for ltac2 references
   that are described in :ref:`ltac2_built-in-quotations`
   (`#10324 <https://github.com/coq/coq/pull/10324>`_,
   fixes `#10088 <https://github.com/coq/coq/issues/10088>`_,
diff --git a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
index 5e005742fd..424540b46a 100644
--- a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
+++ b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
@@ -1,4 +1,5 @@
-- Generalize tactics :tacn:`under` and :tacn:`over` for any registered
+- **Added:**
+  Generalize tactics :tacn:`under` and :tacn:`over` for any registered
   relation. More precisely, assume the given context lemma has type
   `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`.  The
   first step performed by :tacn:`under` (since Coq 8.10) amounts to
diff --git a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst
index 7366ef1190..1dbb3035ce 100644
--- a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst
+++ b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst
@@ -1,3 +1,4 @@
-- Add a :g:`void` notation for the standard library empty type (:g:`Empty_set`)
+- **Added:**
+  A :g:`void` notation for the standard library empty type (:g:`Empty_set`)
   (`#10932 <https://github.com/coq/coq/pull/10932>`_, by Arthur Azevedo de
   Amorim).
diff --git a/doc/changelog/06-ssreflect/11136-inj_compr.rst b/doc/changelog/06-ssreflect/11136-inj_compr.rst
index b546fcde6b..7ebf95b988 100644
--- a/doc/changelog/06-ssreflect/11136-inj_compr.rst
+++ b/doc/changelog/06-ssreflect/11136-inj_compr.rst
@@ -1,2 +1,2 @@
-- Added lemma :g:`inj_compr` to :g:`ssr.ssrfun`
+- **Added:** Lemma :g:`inj_compr` to :g:`ssr.ssrfun`
   (`#11136 <https://github.com/coq/coq/pull/11136>`_, by Cyril Cohen).
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 1c91800c65..cd94bb0513 100644
--- a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst
+++ b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst
@@ -1,4 +1,5 @@
-- Deprecated flag `Refine Instance Mode` has been removed.
+- **Removed:**
+  Deprecated flag `Refine Instance Mode`
   (`#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
diff --git a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst
index c69cda9656..366f799c59 100644
--- a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst
+++ b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst
@@ -1,2 +1,3 @@
-- Remove undocumented :n:`Instance : !@type` syntax
+- **Removed:**
+  Undocumented :n:`Instance : !@type` syntax
   (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/07-commands-and-options/10277-no-show-script.rst b/doc/changelog/07-commands-and-options/10277-no-show-script.rst
index 7fdeb632b4..ee870df607 100644
--- a/doc/changelog/07-commands-and-options/10277-no-show-script.rst
+++ b/doc/changelog/07-commands-and-options/10277-no-show-script.rst
@@ -1,2 +1,3 @@
-- Remove ``Show Script`` command (deprecated since 8.10)
+- **Removed:**
+  Deprecated ``Show Script`` command
   (`#10277 <https://github.com/coq/coq/pull/10277>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/07-commands-and-options/10291-typing-flags.rst b/doc/changelog/07-commands-and-options/10291-typing-flags.rst
index ef7adde801..7dc7def4b3 100644
--- a/doc/changelog/07-commands-and-options/10291-typing-flags.rst
+++ b/doc/changelog/07-commands-and-options/10291-typing-flags.rst
@@ -1,4 +1,5 @@
-- Adding unsafe commands to enable/disable guard checking, positivity checking
+- **Added:**
+  Unsafe commands to enable/disable guard checking, positivity checking
   and universes checking (providing a local `-type-in-type`).
-  See :ref:`controlling-typing-flags`.
+  See :ref:`controlling-typing-flags`
   (`#10291 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier).
diff --git a/doc/changelog/07-commands-and-options/10476-fix-export.rst b/doc/changelog/07-commands-and-options/10476-fix-export.rst
index ba71e1c337..af38008a88 100644
--- a/doc/changelog/07-commands-and-options/10476-fix-export.rst
+++ b/doc/changelog/07-commands-and-options/10476-fix-export.rst
@@ -1,5 +1,6 @@
-- Fix two bugs in `Export`. This can have an impact on the behavior of the
-  `Import` command on libraries. `Import A` when `A` imports `B` which exports
-  `C` was importing `C`, whereas `Import` is not transitive. Also, after
+- **Fixed:**
+  Two bugs in :cmd:`Export`. This can have an impact on the behavior of the
+  :cmd:`Import` command on libraries. `Import A` when `A` imports `B` which exports
+  `C` was importing `C`, whereas :cmd:`Import` is not transitive. Also, after
   `Import A B`, the import of `B` was sometimes incomplete.
   (`#10476 <https://github.com/coq/coq/pull/10476>`_, by Maxime Dénès).
diff --git a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst
index 580e808baa..a17f1704fe 100644
--- a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst
+++ b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst
@@ -1,4 +1,5 @@
-- Update output generated by :flag:`Printing Dependent Evars Line` flag
+- **Changed:**
+  Output generated by :flag:`Printing Dependent Evars Line` flag
   used by the Prooftree tool in Proof General.
   (`#10489 <https://github.com/coq/coq/pull/10489>`_,
   closes `#4504 <https://github.com/coq/coq/issues/4504>`_,
diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst
index c1df728c5c..69a9c40c3c 100644
--- a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst
+++ b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst
@@ -1,4 +1,5 @@
-- Optionally highlight the differences between successive proof steps in the
+- **Added:**
+  Optionally highlight the differences between successive proof steps in the
   :cmd:`Show Proof` command.  Experimental; only available in coqtop
   and Proof General for now, may be supported in other IDEs
   in the future.
diff --git a/doc/changelog/07-commands-and-options/11187-remove-addpath.rst b/doc/changelog/07-commands-and-options/11187-remove-addpath.rst
index 283c44fda6..58c53e3b1d 100644
--- a/doc/changelog/07-commands-and-options/11187-remove-addpath.rst
+++ b/doc/changelog/07-commands-and-options/11187-remove-addpath.rst
@@ -1,4 +1,4 @@
-- Removed legacy commands ``AddPath``, ``AddRecPath``, and ``DelPath``
+- **Removed:** Legacy commands ``AddPath``, ``AddRecPath``, and ``DelPath``
   which were undocumented, broken variants of :cmd:`Add LoadPath`,
   :cmd:`Add Rec LoadPath`, and :cmd:`Remove LoadPath`
   (`#11187 <https://github.com/coq/coq/pull/11187>`_,
diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst
index f612096880..83937390fc 100644
--- a/doc/changelog/08-tools/08642-vos-files.rst
+++ b/doc/changelog/08-tools/08642-vos-files.rst
@@ -1,4 +1,5 @@
-- `coqc` now provides the ability to generate compiled interfaces.
+- **Added:**
+  `coqc` now provides the ability to generate compiled interfaces.
   Use `coqc -vos foo.v` to skip all opaque proofs during the
   compilation of `foo.v`, and output a file called `foo.vos`.
   This feature is experimental. It enables working on a Coq file without the need to
diff --git a/doc/changelog/08-tools/10245-require-command-line.rst b/doc/changelog/08-tools/10245-require-command-line.rst
index 54417077f5..ca871bbf6b 100644
--- a/doc/changelog/08-tools/10245-require-command-line.rst
+++ b/doc/changelog/08-tools/10245-require-command-line.rst
@@ -1,4 +1,5 @@
-- Add command line options `-require-import`, `-require-export`,
+- **Added:**
+  Command-line options `-require-import`, `-require-export`,
   `-require-import-from` and `-require-export-from`, as well as their
   shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate
   confusing command line option `-require`
diff --git a/doc/changelog/08-tools/10947-coq-makefile-dep.rst b/doc/changelog/08-tools/10947-coq-makefile-dep.rst
index f620b32cb8..c59f1312d1 100644
--- a/doc/changelog/08-tools/10947-coq-makefile-dep.rst
+++ b/doc/changelog/08-tools/10947-coq-makefile-dep.rst
@@ -1,4 +1,5 @@
-- Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile`
+- **Changed:**
+  Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile`
   utility, where `<CoqMakefile>` is the name of the output file given by the
   `-o` option. In this way two generated makefiles can coexist in the same
   directory.
diff --git a/doc/changelog/08-tools/11068-coqbin-noslash.rst b/doc/changelog/08-tools/11068-coqbin-noslash.rst
index c2c8f4df31..cd48f9d606 100644
--- a/doc/changelog/08-tools/11068-coqbin-noslash.rst
+++ b/doc/changelog/08-tools/11068-coqbin-noslash.rst
@@ -1,3 +1,3 @@
-- ``coq_makefile`` now supports environment variable ``COQBIN`` with
+- **Fixed:** ``coq_makefile`` now supports environment variable ``COQBIN`` with
   no ending ``/`` character (`#11068
   <https://github.com/coq/coq/pull/11068>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst
index 7babcdb6f1..4b9eb55cbd 100644
--- a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst
+++ b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst
@@ -1,4 +1,5 @@
--  Moved the `auto` hints of the `OrderedType` module into a new `ordered_type`
-   database
-   (`#9772 <https://github.com/coq/coq/pull/9772>`_,
-   by Vincent Laporte).
+- **Changed:**
+  Moved the :tacn:`auto` hints of the `OrderedType` module into a new `ordered_type`
+  database
+  (`#9772 <https://github.com/coq/coq/pull/9772>`_,
+  by Vincent Laporte).
diff --git a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst
index ab625b9e03..8cfd826be0 100644
--- a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst
+++ b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst
@@ -1,4 +1,4 @@
-- Removes deprecated modules `Coq.ZArith.Zlogarithm`
-  and `Coq.ZArith.Zsqrt_compat`
-  (#9881 <https://github.com/coq/coq/pull/9811>
+- **Removed:**
+  Deprecated modules `Coq.ZArith.Zlogarithm` and `Coq.ZArith.Zsqrt_compat`
+  (`#9881 <https://github.com/coq/coq/pull/9811>`_,
   by Vincent Laporte).
diff --git a/doc/changelog/10-standard-library/10445-constructive-reals.rst b/doc/changelog/10-standard-library/10445-constructive-reals.rst
index d69056fc2f..182f8a805c 100644
--- a/doc/changelog/10-standard-library/10445-constructive-reals.rst
+++ b/doc/changelog/10-standard-library/10445-constructive-reals.rst
@@ -1,12 +1,17 @@
-- New module `Reals.ConstructiveCauchyReals` defines constructive real numbers
-  by Cauchy sequences of rational numbers. Classical real numbers are now defined
+- **Added:**
+  Module `Reals.ConstructiveCauchyReals` defines constructive real numbers
+  by Cauchy sequences of rational numbers
+  (`#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria,
+  with the help and review of Guillaume Melquiond and Bas Spitters).
+
+- **Changed:** Classical real numbers are now defined
   as a quotient of these constructive real numbers, which significantly reduces
   the number of axioms needed (see `Reals.Rdefinitions` and `Reals.Raxioms`),
   while preserving backward compatibility.
 
   Futhermore, the new axioms for classical real numbers include the limited
   principle of omniscience (`sig_forall_dec`), which is a logical principle
-  instead of an ad hoc property of the real numbers.
+  instead of an *ad hoc* property of the real numbers.
 
-  See `#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria,
-  with the help and review of Guillaume Melquiond and Bas Spitters.
+  (`#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria,
+  with the help and review of Guillaume Melquiond and Bas Spitters)
diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
index 864c4e6a7e..768fc46714 100644
--- a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
+++ b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
@@ -1,6 +1,9 @@
-- New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and
-  :g:`nth_error` functions on lists. The lemma :g:`filter_app` was moved to the
-  :g:`List` module.
+- **Added:**
+  New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and
+  :g:`nth_error` functions on lists
+  (`#10651 <https://github.com/coq/coq/pull/10651>`_, and
+  `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash).
 
-  See `#10651 <https://github.com/coq/coq/pull/10651>`_, and
-  `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash.
+- **Changed:**
+  The lemma :g:`filter_app` was moved to the :g:`List` module
+  (`#10651 <https://github.com/coq/coq/pull/10651>`_, by Oliver Nash).
diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst
index 5d8467025b..11efef4de0 100644
--- a/doc/changelog/10-standard-library/10827-dedekind-reals.rst
+++ b/doc/changelog/10-standard-library/10827-dedekind-reals.rst
@@ -1,4 +1,5 @@
-- New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers
+- **Added:**
+  New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers
   as boolean-values functions along with 3 logical axioms: limited principle
   of omniscience, excluded middle of negations and functional extensionality.
   The exposed type :g:`R` in module :g:`Reals.Rdefinitions` is those
@@ -6,6 +7,6 @@
   Classical Dedekind reals are a quotient of constructive reals, which allows
   to transport many constructive proofs to the classical case.
 
-  See `#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria,
+  (`#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria,
   based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin,
-  code review by Hugo Herbelin.
+  code review by Hugo Herbelin).
diff --git a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst
index 6e87ff93c7..8aef859ec8 100644
--- a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst
+++ b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst
@@ -1 +1,4 @@
-- ClassicalFacts: Adding the standard equivalence between weak excluded-middle and the classical instance of De Morgan's law (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin).
+- **Added:**
+  Standard equivalence between weak excluded-middle and the
+  classical instance of De Morgan's law, in module :g:`ClassicalFacts`
+  (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin).
diff --git a/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst b/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst
index 8bfd01d7a0..58038eab82 100644
--- a/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst
+++ b/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst
@@ -1,5 +1,5 @@
-- Coq now officially supports OCaml 4.08.
-
-  see INSTALL files for details
+- **Changed:**
+  Coq now officially supports OCaml 4.08.
+  See `INSTALL` file for details
   (`#10471 <https://github.com/coq/coq/pull/10471>`_,
   by Emilio Jesús Gallego Arias).
diff --git a/doc/changelog/README.md b/doc/changelog/README.md
index 3e0970a656..05bf710f89 100644
--- a/doc/changelog/README.md
+++ b/doc/changelog/README.md
@@ -15,12 +15,12 @@ entry in [`dev/doc/changes.md`](../../dev/doc/changes.md).
 ## How to add an entry? ##
 
 Run `./dev/tools/make-changelog.sh`: it will ask you for your PR
-number, and to choose among the predefined categories.  Afterward,
-fill in the automatically generated entry with a short description of
-your change (which should describe any compatibility issues in
-particular).  You may also add a reference to the relevant fixed
-issue, and credit reviewers, co-authors, and anyone who helped advance
-the PR.
+number, and to choose among the predefined categories, and the
+predefined types of changes.  Afterward, fill in the automatically
+generated entry with a short description of your change (which should
+describe any compatibility issues in particular).  You may also add a
+reference to the relevant fixed issue, and credit reviewers,
+co-authors, and anyone who helped advance the PR.
 
 The format for changelog entries is the same as in the reference
 manual.  In particular, you may reference the documentation you just
@@ -31,10 +31,18 @@ manual for details.
 Here is a summary of the structure of a changelog entry:
 
 ``` rst
-- Description of the changes, with possible link to
+- **Added / Changed / Deprecated / Fixed / Removed:**
+  Description of the changes, with possible link to
   :ref:`relevant-section` of the updated documentation
   (`#PRNUM <https://github.com/coq/coq/pull/PRNUM>`_,
   [fixes `#ISSUE1 <https://github.com/coq/coq/issues/ISSUE1>`_
   [ and `#ISSUE2 <https://github.com/coq/coq/issues/ISSUE2>`_],]
   by Full Name[, with help / review of Full Name]).
 ```
+
+The first line indicates the type of change.  Available types come
+from the [Keep a Changelog
+1.0.0](https://keepachangelog.com/en/1.0.0/) specification.  We
+exclude the "Security" type for now because of the absence of a
+process for handling critical bugs (proof of False) as security
+vulnerabilities.