From 2d1cd80305c410ae41b248135d3ddf9505fbf107 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Sep 2016 09:37:06 +0200
Subject: [PATCH] Document iInduction.

---
 ProofMode.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/ProofMode.md b/ProofMode.md
index 9232ac054..4f14da9f3 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -100,6 +100,13 @@ The later modality
 - `iLöb (x1 ... xn) as "IH"` : perform Löb induction by generalizing over the
   Coq level variables `x1 ... xn` and the entire spatial context.
 
+Induction
+---------
+- `iInduction x as cpat "IH"` : perform induction on the Coq term `x`. The Coq
+  introduction pattern is used to name the introduced variables. The induction
+  hypotheses are inserted into the persistent context and given fresh names
+  prefixed `IH`.
+
 Rewriting
 ---------
 
-- 
GitLab