Skip to content
Snippets Groups Projects
Commit acaaa588 authored by Armaël Guéneau's avatar Armaël Guéneau
Browse files

docs/proof_guide.md: fix broken link

parent 20047cf1
No related branches found
No related tags found
No related merge requests found
...@@ -81,7 +81,7 @@ avoided. ...@@ -81,7 +81,7 @@ avoided.
## Type class resolution control ## Type class resolution control
When you are writing a module that exports some Iris term for others to use 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 sure to mark these terms as opaque for type class search at the *end* of your
module (and outside any section): module (and outside any section):
```coq ```coq
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment