Commit 7e9c378e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More proof mode docs.

parent 1a17276b
......@@ -56,6 +56,8 @@ Elimination of logical connectives
quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
object level connectives using the proof mode introduction patterns
`ipat1 ... ipatn`.
- `iDestruct trm as %cpat : elimination of a pure hypothesis using the Coq
introduction pattern `cpat`.
Separating logic specific tactics
Supports Markdown
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