[changelog] Add types to changelog entries.

Types of changes are defined in the list defined by Keep a Changelog
1.0.0 (https://keepachangelog.com/en/1.0.0/):

- Added
- Changed
- Deprecated
- Fixed
- Removed

We exclude the type Security for now, even for soundness fixes,
because the process of handling security vulnerabilities is different
from anything we follow right now.

10 files changed, 30 insertions, 18 deletions

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).