diff --git a/README.md b/README.md
index 94d6075c6c6133687915a16535f586bd68b782e9..ccb04694a1e5eb54c009140518524187be5bfdc7 100644
--- a/README.md
+++ b/README.md
@@ -9,7 +9,7 @@ For using the Coq library, check out the
 
 For understanding the theory of Iris, a LaTeX version of the core logic
 definitions and some derived forms is available in
-[docs/iris.tex](tex/iris.tex).  A compiled PDF version of this document is
+[tex/iris.tex](tex/iris.tex).  A compiled PDF version of this document is
 [available online](http://plv.mpi-sws.org/iris/appendix-3.2.pdf).
 
 ## Building Iris
@@ -83,7 +83,7 @@ followed by `make build-dep`.
   [MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
   intuitionistic and spatial BI++ assertions. It also contains tactics for
   interactive proofs. Documentation can be found in
-  [ProofMode.md](docs/proof_mode.md).
+  [proof_mode.md](docs/proof_mode.md).
 * 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
@@ -137,7 +137,7 @@ Contacting the developers:
 Miscellaneous:
 
 * Information on how to set up your editor for unicode input and output is
-  collected in [Editor.md](docs/editor.md).
+  collected in [editor.md](docs/editor.md).
 * If you are writing a paper that uses Iris in one way or another, you could use
   the [Iris LaTeX macros](tex/iris.sty) for typesetting the various Iris
   connectives.
diff --git a/docs/heap_lang.md b/docs/heap_lang.md
index e3522e3697a0535d0d7c1dee141f3f2bef71fefe..682410d3af968e3be02be4fa8ed072659dcef09f 100644
--- a/docs/heap_lang.md
+++ b/docs/heap_lang.md
@@ -100,7 +100,7 @@ Further tactics:
   the goal is for a single, atomic operation -- `wp_bind` can be used to bring
   the goal into the right shape.
 - `wp_apply pm_trm`: Apply a lemma whose conclusion is a `WP`, automatically
-  applying `wp_bind` as needed.  See the [ProofMode docs](ProofMode.md) for an
+  applying `wp_bind` as needed.  See the [ProofMode docs](./proof_mode.md) for an
   explanation of `pm_trm`.
 
 There is no tactic for `Fork`, just do `wp_apply wp_fork`.
diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index 81fb498200900d22efc02a757c45d50053a24422..c3de717617a0d6e57fd73159f2a2d768dc456947 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -2,9 +2,9 @@
 
 This work-in-progress document serves to explain how Iris proofs are typically
 carried out in Coq: what are the common patterns, what are the common pitfalls.
-This complements the tactic documentation for the [proof mode](ProofMode.md) and
-[HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in
-the [style guide](StyleGuide.md).
+This complements the tactic documentation for the [proof mode](./proof_mode.md) and
+[HeapLang](./heap_lang.md) as well as the documentation of syntactic conventions in
+the [style guide](./style_guide.md).
 
 ## Order of `Requires`
 
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 990a7a44eaed48b72d2252c0cfcbe56134a1a67b..60229568a98bbe68fca7dcde6c0890803834bd82 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -3,7 +3,7 @@ Tactic overview
 
 Many of the tactics below apply to more goals than described in this document
 since the behavior of these tactics can be tuned via instances of the type
-classes in the file [proofmode/classes](proofmode/classes.v). Most notably, many
+classes in the file [proofmode/classes](theories/proofmode/classes.v). Most notably, many
 of the tactics can be applied when the connective to be introduced or to be eliminated
 appears under a later, an update modality, or in the conclusion of a
 weakest precondition.
@@ -260,12 +260,12 @@ For example, given:
 
 You can write
 
-        iIntros (x Hx) "!# $ [[] | #[HQ HR]] /= !>".
+        iIntros (x Hx) "!> $ [[] | #[HQ HR]] /= !>".
 
 which results in:
 
         x : nat
-        H : x = 0
+        Hx : x = 0
         ______________________________________(1/1)
         "HQ" : Q
         "HR" : R
@@ -361,4 +361,4 @@ HeapLang tactics
 ================
 
 If you came here looking for the `wp_` tactics, those are described in the
-[HeapLang documentation](HeapLang.md).
+[HeapLang documentation](./heap_lang.md).
diff --git a/docs/style_guide.md b/docs/style_guide.md
index f6bae4b6c9bb6892a7cf6599312f1bcd8693b205..65fd057598f6b9127b485631b021bf9c4776c62e 100644
--- a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ -2,8 +2,8 @@
 
 This document lays down syntactic conventions about how we usually write our
 Iris proofs in Coq.  It is a work-in-progress.  This complements the tactic
-documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as
-well as the [proof guide](ProofGuide.md).
+documentation for the [proof mode](./proof_mode.md) and [HeapLang](./heap_lang.md) as
+well as the [proof guide](.doco/proof_guide.md).
 
 ## Implicit generalization
 
@@ -114,8 +114,8 @@ is used by clients.
 * R: cameras
 * UR: unital cameras or resources algebras
 * F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
-* G: global camera functor management (typeclass; see `ProofGuide.md`)
+* G: global camera functor management (typeclass; see [proof\_guide.md](./proof_guide.md))
 * I: bunched implication logic (of type `bi`)
 * SI: step-indexed bunched implication logic (of type `sbi`)
 * T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
-* Σ: global camera functor management (`gFunctors`; see `ProofGuide.md`)
+* Σ: global camera functor management (`gFunctors`; see [proof\_guide.md](./proof_guide.md))