diff --git a/ProofMode.md b/ProofMode.md
index 6e2c229704098f2dd4fb118df7d323b216f46886..29807cb9eda3442bd4f13cc722aa2f2190f59d02 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.