diff --git a/ProofMode.md b/ProofMode.md
index a7fa7c4376790efb01f4ab36d0b1f163e660ac2a..8583f742e2cf6b95ca15d4d1c3c4cd727a042de7 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -123,10 +123,10 @@ The later modality
   hypotheses. If the argument `n` is not given, it strips one later if the
   leftmost conjuct is of the shape `â–· P`, or `n` laters if the leftmost conjuct
   is of the shape `â–·^n P`.
-- `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction by generating a
-  hypothesis `IH : â–· goal`. The tactic generalizes over the Coq level variables
-  `x1 ... xn`, the hypotheses given by the selection pattern `selpat`, and the
-  spatial context.
+- `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
+  generating a hypothesis `IH : â–· goal`. The tactic generalizes over the Coq
+  level variables `x1 ... xn`, the hypotheses given by the selection pattern
+  `selpat`, and the spatial context.
 
 Induction
 ---------