Skip to content
Snippets Groups Projects
Commit d62f14ed authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Markdown nits in ProofMode.md

parent 9e6ebe60
No related branches found
No related tags found
No related merge requests found
......@@ -171,8 +171,8 @@ Iris
----
- `iInv S with "selpat" as (x1 ... xn) "ipat" "Hclose"` : where `S` is either
a namespace N or an identifier "H". Open the invariant indicated by S. The
selection pattern `selpat` is used for any auxiliary assertions needed to
a namespace `N` or an identifier `H`. Open the invariant indicated by `S`.
The selection pattern `selpat` is used for any auxiliary assertions needed to
open the invariant (e.g. for cancelable or non-atomic invariants). The update
for closing the invariant is put in a hypothesis named `Hclose`.
......
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