3 files changed, 16 insertions, 9 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 0506216541..8b0bf216e3 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -18,10 +18,6 @@ Dune will get confused if it finds leftovers of in-tree compilation,
 so please be sure your tree is clean from objects files generated by
 the make-based system.
 
-If you want to build the standard libraries and plugins you should
-call `make -f Makefile.dune voboot`. It is usually enough to do that
-once per-session.
-
 More helper targets are available in `Makefile.dune`, `make -f
 Makefile.dune` will display some help.
 
@@ -55,7 +51,6 @@ Instead, you should use the provided "shims" for running `coqtop` and
 `coqide` in a fast build. In order to use them, do:
 
 ```
-$ make -f Makefile.dune voboot                # Only once per session
 $ dune exec -- dev/shim/coqtop-prelude
 ```
 
@@ -153,7 +148,7 @@ depending on your OCaml version. This is due to several factors:
 
 ## Dropping from coqtop:
 
-After doing `make -f Makefile.dune voboot`, the following commands should work:
+The following commands should work:
 ```
 dune exec -- dev/shim/coqbyte-prelude
 > Drop.
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index eac8d86b0a..9498ab8bbb 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -9,6 +9,13 @@
 
 ### ML API
 
+Proof state and constant declaration:
+
+- A large consolidation of the API handling interactive and
+  non-interactive constant has been performed; low-level APIs are no
+  longer available, and the functionality of the `Proof_global` module
+  has been merged into `Declare`.
+
 Notations:
 
 - Most operators on numerals have moved to file numTok.ml.
@@ -68,7 +75,6 @@ Proof state:
   information related to the constant declaration. Some functions have
   been renamed from `start_proof` to `start_lemma`
 
-
   Plugins that require access to the information about currently
   opened lemmas can add one of the `![proof]` attributes to their
   `mlg` entry, which will refine the type accordingly. See
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 58c2fcc68a..340b66bbd0 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -96,6 +96,8 @@ in time.
 - [ ] Delay non-blocking issues to the appropriate milestone and ensure
   blocking issues are solved. If required to solve some blocking issues,
   it is possible to revert some feature PRs in the version branch only.
+- [ ] Add a new link to the ``'versions'`` list of the refman (in
+      ``html_context`` in ``doc/sphinx/conf.py``).
 
 ## Before the beta release date ##
 
@@ -131,8 +133,12 @@ in time.
   the package managers can Cc `@erikmd` to request that he prepare the necessary configuration for the Docker release in [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq)
   (namely, he'll need to make sure a `coq-bignums` opam package is available in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), respectively [`released`](https://github.com/coq/opam-coq-archive/tree/master/released), so the Docker image gathering `coq` and `coq-bignums` can be built).
 - [ ] Draft a release on GitHub.
-- [ ] Get `@maximedenes` to sign the Windows and MacOS packages and
-  upload them on GitHub.
+- [ ] Sign the Windows and MacOS packages and upload them on GitHub.
+  + The Windows packages must be signed by the Inria IT security service. They
+    should be sent as a link to the binary together with its SHA256 hash in a
+    signed e-mail, via our local contact (currently `@maximedenes`).
+  + The MacOS packages should be signed by our own certificate, by sending them
+    to `@maximedenes`. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases).
 - [ ] Prepare a page of news on the website with the link to the GitHub release
   (see [coq/www#63](https://github.com/coq/www/pull/63)).
 - [ ] Upload the new version of the reference manual to the website.