diff --git a/ProofMode.md b/ProofMode.md
index 6e2c229704098f2dd4fb118df7d323b216f46886..2071dd3512d1aa4b5c806652b0b24d2e0dbc51cb 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.
@@ -113,7 +113,7 @@ Modalities
----------
- `iModIntro` : introduction of a modality that is an instance of the
- `IntoModal` type class. Instances include: later, except 0, basic update and
+ `FromModal` type class. Instances include: later, except 0, basic update and
fancy update.
- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
an instance of the `ElimModal` type class. Instances include: later, except 0,