From 6ab7c43650fe17bc62d950138e94c0cb9caa6a90 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Thu, 16 Mar 2017 10:49:59 +0100
Subject: [PATCH] Updated the notation for lifting in ProofMode docs

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

diff --git a/ProofMode.md b/ProofMode.md
index 6e2c22970..29807cb9e 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -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.
-- 
GitLab