diff --git a/ProofMode.md b/ProofMode.md
index 692c7568c722f394b6b8583917106495b67bb791..8ffaa46bcddc4e7128d542186ac51af889cae173 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -56,6 +56,8 @@ Elimination of logical connectives
   quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
   object level connectives using the proof mode introduction patterns
   `ipat1 ... ipatn`.
+- `iDestruct trm as %cpat : elimination of a pure hypothesis using the Coq
+   introduction pattern `cpat`.
 
 Separating logic specific tactics
 ---------------------------------