From 01db4f64b8eeac617ad34c3ab6147bee0fc45579 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Sep 2019 08:28:08 +0200
Subject: [PATCH] =?UTF-8?q?Proof=20mode=20docs:=20COFE=20=E2=86=92=20OFE,?=
 =?UTF-8?q?=20CMRA=20=E2=86=92=20camera.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 ProofMode.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ProofMode.md b/ProofMode.md
index 5014c1958..7c6be416c 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -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.
-- 
GitLab