diff --git a/ProofMode.md b/ProofMode.md
index b165c01a5cd895cf2126ffd4aff53844e8849312..9d2220a73c379e5d46582ad014348b4de3a5565f 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -111,6 +111,9 @@ Separation logic-specific tactics
   framed.
 - `iCombine "H1" "H2" as "pat"` : combines `H1 : P1` and `H2 : P2` into
   `H: P1 ∗ P2`, then calls `iDestruct H as pat` on the combined hypothesis.
+- `iAccu` : solves a goal that is an evar by instantiating it with a all
+  hypotheses from the spatial context joined together with a separating
+  conjunction (or `emp` in case the spatial context is empty).
 
 Modalities
 ----------