diff --git a/ProofMode.md b/ProofMode.md
index 5014c1958231b91a058dea8b6710892d506d9927..7c6be416c8cd9836cff6a40328788aec897c7148 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.