From 250619574eb77967930f8f791390fa79ced5f581 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 18 Feb 2020 21:54:04 +0100
Subject: [PATCH] Improve docs of the `# pat` intro pattern.
---
docs/proof_mode.md | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 60229568..1767f1a8 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -234,7 +234,12 @@ _introduction patterns_:
- `[]` : false elimination.
- `%` : move the hypothesis to the pure Coq context (anonymously).
- `->` and `<-` : rewrite using a pure Coq equality
-- `# ipat` : move the hypothesis into the intuitionistic context.
+- `# ipat` : move the hypothesis into the intuitionistic context. The tactic
+ will fail if the hypothesis is not intuitionistic. On success, the tactic will
+ strip any number of intuitionistic and persistence modalities. If the
+ hypothesis is already in the intuitionistic context, the tactic will still
+ strip intuitionistic and persistence modalities (it is a no-op if the
+ hypothesis does not contain such modalities).
- `> ipat` : eliminate a modality (if the goal permits).
Apart from this, there are the following introduction patterns that can only
--
GitLab