diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 6d16ae1ba47ddbb9f089c364f29cf0f6676542da..4407a6cd1379c49837974667139206f3b35d5b50 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -240,7 +240,7 @@ Induction
   + `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction,
   generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
   the selection pattern `selpat`, and the spatial context as usual.
-- `iInduction x as cpat "selpat"` : perform induction on the Coq term `x`. The
+- `iInduction x as cpat` : perform induction on the Coq term `x`. The
   Coq introduction pattern `cpat` is used to name the introduced variables,
   including the induction hypotheses which are introduced into the proof mode
   context. Note that induction hypotheses should not be put into string