diff --git a/README.md b/README.md
index e01c64e530a3b61190265ae28883ee5a9b56878e..ccaabe142f742aa2b1d34da725d9c328a51b9045 100644
--- a/README.md
+++ b/README.md
@@ -20,33 +20,35 @@ Run `make` to build the full development.
## Structure
-* The folder [prelude](prelude) contains an extended "Standard Library" by
- [Robbert Krebbers](http://robbertkrebbers.nl/thesis.html).
-* The folder [algebra](algebra) contains the COFE and CMRA constructions as well
- as the solver for recursive domain equations.
-* The folder [base_logic](base_logic) defines the Iris base logic and the
- primitive connectives. It also contains derived constructions that are
+* The folder [prelude](theories/prelude) contains an extended "Standard Library"
+ by [Robbert Krebbers](http://robbertkrebbers.nl/thesis.html).
+* The folder [algebra](theories/algebra) contains the COFE and CMRA
+ constructions as well as the solver for recursive domain equations.
+* The folder [base_logic](theories/base_logic) defines the Iris base logic and
+ the primitive connectives. It also contains derived constructions that are
entirely independent of the choice of resources.
- * The subfolder [lib](base_logic/lib) contains some generally useful
+ * The subfolder [lib](theories/base_logic/lib) contains some generally useful
derived constructions. Most importantly, it defines composeable
dynamic resources and ownership of them; the other constructions depend
on this setup.
-* The folder [program_logic](program_logic) specializes the base logic to build
- Iris, the program logic. This includes weakest preconditions that are
- defined for any language satisfying some generic axioms, and some derived
+* The folder [program_logic](theories/program_logic) specializes the base logic
+ to build Iris, the program logic. This includes weakest preconditions that
+ are defined for any language satisfying some generic axioms, and some derived
constructions that work for any such language.
-* The folder [proofmode](proofmode) contains the Iris proof mode, which extends
- Coq with contexts for persistent and spatial Iris assertions. It also contains
- tactics for interactive proofs in Iris. Documentation can be found in
+* The folder [proofmode](theories/proofmode) contains the Iris proof mode, which
+ extends Coq with contexts for persistent and spatial Iris assertions. It also
+ contains tactics for interactive proofs in Iris. Documentation can be found in
[ProofMode.md](ProofMode.md).
-* The folder [heap_lang](heap_lang) defines the ML-like concurrent heap language
- * The subfolder [lib](heap_lang/lib) contains a few derived constructions
- within this language, e.g., parallel composition.
- Most notable here is [lib/barrier](heap_lang/lib/barrier), the implementation
- and proof of a barrier as described in .
-* The folder [tests](tests) contains modules we use to test our infrastructure.
- Users of the Iris Coq library should *not* depend on these modules; they may
- change or disappear without any notice.
+* The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
+ language
+ * The subfolder [lib](theories/heap_lang/lib) contains a few derived
+ constructions within this language, e.g., parallel composition.
+ Most notable here is [lib/barrier](theories/heap_lang/lib/barrier), the
+ implementation and proof of a barrier as described in
+ .
+* The folder [tests](theories/tests) contains modules we use to test our
+ infrastructure. Users of the Iris Coq library should *not* depend on these
+ modules; they may change or disappear without any notice.
## Documentation