diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 60229568a98bbe68fca7dcde6c0890803834bd82..1767f1a8cffa5915620a1f5e83453ed360195c2a 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