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

Remove useless newlines in `proof_mode.md`.

parent 91cfdc1e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 2 deletions
docs/proof_mode.md
+ 0
− 2
View file @ 1a5d7d58
...@@ -72,10 +72,8 @@ Introduction of logical connectives ...@@ -72,10 +72,8 @@ Introduction of logical connectives
- `iPureIntro` : turn a pure goal into a Coq goal. This tactic works for goals - `iPureIntro` : turn a pure goal into a Coq goal. This tactic works for goals
of the shape `⌜φ⌝`, `a ≡ b` on discrete OFEs, and `✓ a` on discrete cameras. of the shape `⌜φ⌝`, `a ≡ b` on discrete OFEs, and `✓ a` on discrete cameras.
- `iLeft` : left introduction of disjunction. - `iLeft` : left introduction of disjunction.
- `iRight` : right introduction of disjunction. - `iRight` : right introduction of disjunction.
- `iSplit` : introduction of a conjunction, or separating conjunction provided - `iSplit` : introduction of a conjunction, or separating conjunction provided
one of the operands is persistent. one of the operands is persistent.
- `iSplitL "H1 ... Hn"` : introduction of a separating conjunction. The - `iSplitL "H1 ... Hn"` : introduction of a separating conjunction. The
......
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