diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 4d5e348b4b64fc1bd2f1f294364c635aba9a01b7..f7d8805bee7a629db433611d61cd3d746887c396 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -5,12 +5,41 @@ Discussion about the Iris Coq development happens on the mailing list
 in the [Iris Chat](https://mattermost.mpi-sws.org/iris).  This is also the right
 place to ask questions.  The chat requires an account at the
 [MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
-tab).
-
-If you want to report a bug, please use the
+tab).  If you want to report a bug, please use the
 [issue tracker](https://gitlab.mpi-sws.org/FP/iris-coq/issues), which also
-requires an MPI-SWS GitLab account.  To contribute code, please send your
-MPI-SWS GitLab username to [Ralf Jung](https://gitlab.mpi-sws.org/jung) to
-enable personal projects for your account.  Then you can fork the
+requires an MPI-SWS GitLab account.
+
+## How to submit a merge request
+
+To contribute code, please send your MPI-SWS GitLab username to
+[Ralf Jung](https://gitlab.mpi-sws.org/jung) to enable personal projects for
+your account.  Then you can fork the
 [Iris git repository](https://gitlab.mpi-sws.org/FP/iris-coq/), make your
 changes in your fork, and create a merge request.
+
+Please do *not* use the master branch of your fork, that might confuse CI.  Use
+a feature branch instead.
+
+## How to update the std++ dependency
+
+* Do the change in std++, push it.
+* Wait for CI to publish a new std++ version on the opam archive, then run
+  `opam update iris-dev`.
+* In Iris, change the `opam` file to depend on the new version.
+* Run `make build-dep` (in Iris) to install the new version of std++.
+  You may have to do `make clean` as Coq will likely complain about .vo file
+  mismatches.
+
+## How to write/update test cases
+
+The files in `tests/` are test cases.  Each of the `.v` files comes with a
+matching `.ref` file containing the expected output of `coqc`.  Adding `Show.`
+in selected places in the proofs makes `coqc` print the current goal state.
+This is used to make sure the proof mode prints goals and reduces terms the way
+we expect it to.  You can run `MAKE_REF=1 make` to re-generate all the `.ref` files;
+this is useful after adding or removing `Show.` from a test.  If you do this,
+make sure to check the diff for any unexpected changes in the output!
+
+Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
+Coq-8.8-specific `.ref` file).  If you change one of these, remember to update
+*all* the `.ref` files.
diff --git a/README.md b/README.md
index 9ac050820db8e3065277fad3063c782e13790ac6..e99525d7327c672ef89d7fb56e2bf69abf9bba73 100644
--- a/README.md
+++ b/README.md
@@ -114,27 +114,6 @@ that should be compatible with this version:
   collected in [Editor.md](Editor.md).
 * The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
 * Naming conventions are documented at [Naming.md](Naming.md).
+* The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
 
-### How to update the std++ dependency
-
-* Do the change in std++, push it.
-* Wait for CI to publish a new std++ version on the opam archive, then run
-  `opam update iris-dev`.
-* In Iris, change the `opam` file to depend on the new version.
-* Run `make build-dep` (in Iris) to install the new version of std++.
-  You may have to do `make clean` as Coq will likely complain about .vo file
-  mismatches.
-
-### How to write/update test cases
-
-The files in `tests/` are test cases.  Each of the `.v` files comes with a
-matching `.ref` file containing the expected output of `coqc`.  Adding `Show.`
-in selected places in the proofs makes `coqc` print the current goal state.
-This is used to make sure the proof mode prints goals and reduces terms the way
-we expect it to.  You can run `MAKE_REF=1 make` to re-generate all the `.ref` files;
-this is useful after adding or removing `Show.` from a test.  If you do this,
-make sure to check the diff for any unexpected changes in the output!
-
-Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
-Coq-8.8-specific `.ref` file).  If you change one of these, remember to update
-*all* the `.ref` files.
+To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).