Skip to content
Snippets Groups Projects
Commit c4aeb8dd authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'fix_link' into 'master'

docs/proof_guide.md: fix broken link

See merge request iris/iris!859
parents 20047cf1 acaaa588
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