Commit 61ac60d4 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make indentation in proof mode docs consistent.

parent b008a6b2
Pipeline #39027 passed with stage
in 11 minutes and 41 seconds
......@@ -248,8 +248,8 @@ Iris
----
- `iInv H as (x1 ... xn) "ipat"` : open an invariant in hypothesis H. The result
is destructed using the Coq intro patterns `x1 ... xn` (for existential
quantifiers) and then the proof mode [introduction pattern][ipat] `ipat`.
is destructed using the Coq intro patterns `x1 ... xn` (for existential
quantifiers) and then the proof mode [introduction pattern][ipat] `ipat`.
+ `iInv H with "selpat" as (x1 ... xn) "ipat" "Hclose"` : generate an update
for closing the invariant and put it in a hypothesis named `Hclose`.
+ `iInv H with "selpat" as (x1 ... xn) "ipat"` : supply a selection pattern
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment