From af80361b8b78723f6290ad413609709e3fdd54ec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Wed, 4 Jan 2017 18:08:22 +0100
Subject: [PATCH] Missing stuff in Proofmode.md.
Thanks to Janno for spotting this!
---
ProofMode.md | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/ProofMode.md b/ProofMode.md
index a7fa7c43..8583f742 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
---------
--
2.26.2