From 20145c5fb916b1f9fe36f2bcd274e741ccb86e27 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Tue, 25 May 2021 12:32:23 +0000
Subject: [PATCH] Document `iInduction ... using` tactic.
---
docs/proof_mode.md | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 072747345..0ad6ea222 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -240,6 +240,11 @@ Induction
+ `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction,
generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
the selection pattern `selpat`, and the spatial context.
+ + `iInduction x as cpat "IH" using t` : perform induction using the induction
+ scheme `t`. Common examples of induction schemes are `map_ind`, `set_ind_L`,
+ and `gmultiset_ind` for `gmap`, `gset`, and `gmultiset`.
+ + `iInduction x as cpat "IH" using t forall (x1 ... xn) "selpat"` : the above
+ variants combined.
Rewriting / simplification
--------------------------
--
GitLab