From 4e7365ae5ba31f3cb911f8428e56320b8b349592 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Aug 2024 22:29:01 +0200
Subject: [PATCH] Fix error in `iInduction` docs.

---
 docs/proof_mode.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 6d16ae1ba..4407a6cd1 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
-- 
GitLab