diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index 1da235b8b184ed35cff232603e18960a2c356900..e5781758c5023669ebccb95017310a1476b2adff 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -81,7 +81,7 @@ avoided.
 ## Type class resolution control
 
 When you are writing a module that exports some Iris term for others to use
-(e.g., `join_handle` in the [spawn module](../theories/heap_lang/lib/spawn.v)), be
+(e.g., `join_handle` in the [spawn module](../iris_heap_lang/lib/spawn.v)), be
 sure to mark these terms as opaque for type class search at the *end* of your
 module (and outside any section):
 ```coq