diff --git a/README.md b/README.md
index 61ce577beb3ca653b94ae570591eb0506d2cb72a..b567ead3603db0fc7ac4419ed1a244e21addabd2 100644
--- a/README.md
+++ b/README.md
@@ -28,27 +28,27 @@ running:
## Structure
-* The folder `prelude` contains an extended "Standard Library" by Robbert
- Krebbers .
-* The folder `algebra` contains the COFE and CMRA constructions as well as
- the solver for recursive domain equations.
-* The folder `program_logic` builds the semantic domain of Iris, defines and
- verifies primitive view shifts and weakest preconditions, and builds some
- language-independent derived constructions (e.g., STSs).
-* The folder `heap_lang` defines the ML-like concurrent heap language
- * The subfolder `lib` contains a few derived constructions within this
- language, e.g., parallel composition.
- Most notable here s `lib/barrier`, the implementation and proof of a barrier
- as described in .
-* The folder `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 `tests` contains modules we use to test our infrastructure.
+* The folder [prelude](prelude) contains an extended "Standard Library" by
+ Robbert Krebbers .
+* The folder [algebra](algebra) contains the COFE and CMRA constructions as well
+ as the solver for recursive domain equations.
+* The folder [program_logic](program_logic) builds the semantic domain of Iris,
+ defines and verifies primitive view shifts and weakest preconditions, and
+ builds some language-independent derived constructions (e.g., STSs).
+* 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 s [lib/barrier](heap_lang/lib/barrier), the implementation
+ and proof of a barrier as described in .
+* 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
+ [ProofMode.md](ProofMode.md).
+* 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.
## Documentation
A LaTeX version of the core logic definitions and some derived forms is
-available in [`docs/iris.tex`](docs/iris.tex).
+available in [docs/iris.tex](docs/iris.tex).