3 files changed, 30 insertions, 31 deletions
diff --git a/doc/changelog/README.md b/doc/changelog/README.md
index 2891eb207e..3e0970a656 100644
--- a/doc/changelog/README.md
+++ b/doc/changelog/README.md
@@ -7,25 +7,28 @@ otherwise important infrastructure changes, and important bug fixes
 should get a changelog entry.
 
 Compatibility-breaking changes should always get a changelog entry,
-which should explain what compatibility-breakage is to expect.
+which should explain what compatibility breakage is to expect.
 
 Pull requests changing the ML API in significant ways should add an
 entry in [`dev/doc/changes.md`](../../dev/doc/changes.md).
 
 ## How to add an entry? ##
 
-You should create a file in one of the sub-directories. The name of
-the file should be `NNNNN-identifier.rst` where `NNNNN` is the number
-of the pull request on five digits and `identifier` is whatever you
-want.
-
-This file should use the same format as the reference manual (as it
-will be copied in there). You may reference the documentation you just
-added with `:ref:`, `:tacn:`, `:cmd:`, `:opt:`, `:token:`, etc. See
+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.
+
+The format for changelog entries is the same as in the reference
+manual.  In particular, you may reference the documentation you just
+added with `:ref:`, `:tacn:`, `:cmd:`, `:opt:`, `:token:`, etc.  See
 the [documentation of the Sphinx format](../sphinx/README.rst) of the
 manual for details.
 
-The entry should be written using the following structure:
+Here is a summary of the structure of a changelog entry:
 
 ``` rst
 - Description of the changes, with possible link to
@@ -35,7 +38,3 @@ The entry should be written using the following structure:
   [ and `#ISSUE2 <https://github.com/coq/coq/issues/ISSUE2>`_],]
   by Full Name[, with help / review of Full Name]).
 ```
-
-The description should be kept rather short and the only additional
-required meta-information are the link to the pull request and the
-full name of the author.
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 0148925247..b6fcf9da22 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -198,21 +198,21 @@ Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2)
 with contributions from many users. A list of packages is available at
 https://coq.inria.fr/opam/www/.
 
-The 61 contributors to this version are David A. Dalrymple, Tanaka
-Akira, Benjamin Barenblat, Yves Bertot, Frédéric Besson, Lasse
-Blaauwbroek, Martin Bodin, Joachim Breitner, Tej Chajed, Frédéric
-Chapoton, Arthur Charguéraud, Cyril Cohen, Lukasz Czajka, Christian
-Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Gaëtan Gilbert, Matěj
-Grabovský, Simon Gregersen, Jason Gross, Samuel Gruetter, Hugo Herbelin,
-Jasper Hugunin, Mirai Ikebuchi, Emilio Jesus Gallego Arias, Chantal
-Keller, Matej Košík, Vincent Laporte, Olivier Laurent, Larry Darryl Lee
-Jr, Pierre Letouzey, Nick Lewycky, Yao Li, Yishuai Li, Xia Li-yao, Assia
-Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, Guillaume
-Melquiond, Kayla Ngan, Sam Pablo Kuper, Karl Palmskog, Clément
-Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Ryan
-Scott, Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau,
-Enrico Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo
-Winterhalter, Beta Ziliani and Théo Zimmermann.
+The 61 contributors to this version are Tanaka Akira, Benjamin
+Barenblat, Yves Bertot, Frédéric Besson, Lasse Blaauwbroek, Martin
+Bodin, Joachim Breitner, Tej Chajed, Frédéric Chapoton, Arthur
+Charguéraud, Cyril Cohen, Lukasz Czajka, David A. Dalrymple, Christian
+Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesus Gallego
+Arias, Gaëtan Gilbert, Matěj Grabovský, Simon Gregersen, Jason Gross,
+Samuel Gruetter, Hugo Herbelin, Jasper Hugunin, Mirai Ikebuchi,
+Chantal Keller, Matej Košík, Sam Pablo Kuper, Vincent Laporte, Olivier
+Laurent, Larry Darryl Lee Jr, Nick Lewycky, Yao Li, Yishuai Li, Assia
+Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez,
+Guillaume Melquiond, Kayla Ngan, Karl Palmskog, Pierre-Marie Pédrot,
+Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Ryan Scott,
+Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau, Enrico
+Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo Winterhalter,
+Xia Li-yao, Beta Ziliani and Théo Zimmermann.
 
 Many power users helped to improve the design of the new features via
 the issue and pull request system, the |Coq| development mailing list,
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 47ecfb9db0..9e219bd503 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -62,7 +62,7 @@ A simple example of a ``_CoqProject`` file follows:
     theories/foo.v
     theories/bar.v
     -I src/
-    src/baz.ml4
+    src/baz.mlg
     src/bazaux.ml
     src/qux_plugin.mlpack
 
@@ -111,7 +111,7 @@ decide how to build them. In particular:
 + |Coq| files must use the ``.v`` extension
 + |OCaml| files must use the ``.ml`` or ``.mli`` extension
 + |OCaml| files that require pre processing for syntax
-  extensions (like ``VERNAC EXTEND``) must use the ``.ml4`` extension
+  extensions (like ``VERNAC EXTEND``) must use the ``.mlg`` extension
 + In order to generate a plugin one has to list all |OCaml|
   modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib``
   file).