Commit 6ab7c436 authored by Dan Frumin's avatar Dan Frumin

Updated the notation for lifting in ProofMode docs

parent 3d6525a5
......@@ -57,7 +57,7 @@ Introduction of logical connectives
-----------------------------------
- `iPureIntro` : turn a pure goal into a Coq goal. This tactic works for goals
of the shape `■ φ`, `a ≡ b` on discrete COFEs, and `✓ a` on discrete CMRAs.
of the shape `⌜φ⌝`, `a ≡ b` on discrete COFEs, and `✓ a` on discrete CMRAs.
- `iLeft` : left introduction of disjunction.
- `iRight` : right introduction of disjunction.
......
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