improve README structure

README.md

@@ -3,7 +3,9 @@
 This is the Coq development of the [Iris Project](http://iris-project.org), in
 the MoSeL version.
 
-## Prerequisites
+## Building Iris
+
+### Prerequisites
 
 This version is known to compile with:
 
@@ -15,7 +17,7 @@ For a version compatible with Coq 8.6, have a look at the
 If you need to work with Coq 8.5, please check out the
 [iris-3.0 branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.0).
 
-## Installing via opam
+### Installing via opam
 
 To obtain the latest stable release via opam (1.2.2 or newer), you have to add
 the Coq opam repository:
@@ -28,7 +30,7 @@ To obtain a development version, add the Iris opam repository:
 
     opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
 
-## Building from source
+### Building from source
 
 When building Iris from source, we recommend to use opam (1.2.2 or newer) for
 installing Iris's dependencies.  This requires the following two repositories:
@@ -98,7 +100,9 @@ that should be compatible with this version:
 * [Iris Atomic](https://gitlab.mpi-sws.org/FP/iris-atomic/) is an experimental
   formalization of logically atomic triples in Iris.
 
-## For Developers: How to update the std++ dependency
+## Notes for Iris Developers
+
+### 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
@@ -107,3 +111,13 @@ that should be compatible with this 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` 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!