Commit 01db4f64 authored by Robbert Krebbers's avatar Robbert Krebbers

Proof mode docs: COFE → OFE, CMRA → camera.

parent 0236daec
......@@ -59,7 +59,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 OFEs, and `✓ a` on discrete cameras.
- `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