3 files changed, 29 insertions, 5 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 3f1b470878..c9eceb1270 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -71,8 +71,9 @@ those external projects should have been prepared (cf. the relevant sub-section
 in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
 with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
 
-Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) or
-the [`dev/doc/changes.md`](changes.md) file.
+Moreover the PR author *must* add an entry to the [unreleased
+changelog](../../doc/changelog/README.md) or to the
+[`dev/doc/changes.md`](changes.md) file.
 
 If overlays are missing, ask the author to prepare them and label the PR with
 the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9e0d47651e..7221c3de56 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,10 @@
+## Changes between Coq 8.10 and Coq 8.11
+
+### ML API
+
+- Functions and types deprecated in 8.10 have been removed in Coq
+  8.11.
+
 ## Changes between Coq 8.9 and Coq 8.10
 
 ### ML4 Pre Processing
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 60c0886896..189d6f9fa5 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -84,10 +84,18 @@
   Coq has been tagged.
 - [ ] Have some people test the recently auto-generated Windows and MacOS
   packages.
-- [ ] Change the version name from alpha to beta1 (see
+- [ ] In a PR:
+  - Change the version name from alpha to beta1 (see
   [#7009](https://github.com/coq/coq/pull/7009/files)).
-  We generally do not update the magic numbers at this point.
+  - We generally do not update the magic numbers at this point.
+  - Set `is_a_released_version` to `true` in `configure.ml`.
 - [ ] Put the `VX.X+beta1` tag using `git tag -s`.
+- [ ] Check using `git push --tags --dry-run` that you are not
+  pushing anything else than the new tag. If needed, remove spurious
+  tags with `git tag -d`. When this is OK, proceed with `git push --tags`.
+- [ ] Set `is_a_released_version` to `false` in `configure.ml`
+  (if you forget about it, you'll be reminded whenever you try to
+  backport a PR with a changelog entry).
 
 ### These steps are the same for all releases (beta, final, patch-level) ###
 
@@ -112,9 +120,17 @@
 
 ## At the final release time ##
 
-- [ ] Change the version name to X.X.0 and the magic numbers (see
+- [ ] In a PR:
+  - Change the version name from X.X.0 and the magic numbers (see
   [#7271](https://github.com/coq/coq/pull/7271/files)).
+  - Set `is_a_released_version` to `true` in `configure.ml`.
 - [ ] Put the `VX.X.0` tag.
+- [ ] Check using `git push --tags --dry-run` that you are not
+  pushing anything else than the new tag. If needed, remove spurious
+  tags with `git tag -d`. When this is OK, proceed with `git push --tags`.
+- [ ] Set `is_a_released_version` to `false` in `configure.ml`
+  (if you forget about it, you'll be reminded whenever you try to
+  backport a PR with a changelog entry).
 
 Repeat the generic process documented above for all releases.