diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 1767f1a8cffa5915620a1f5e83453ed360195c2a..019ed7312015217fcd9f451c04d91ba1f6bbcd5e 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -240,6 +240,10 @@ _introduction patterns_:
   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` : move the hypothesis from the intuitionistic context into the
+  spatial context. If the hypothesis is already in the spatial context, the
+  tactic is a no-op. If the hypothesis is not affine, an `<affine>` modality is
+  added to the hypothesis.
 - `> ipat` : eliminate a modality (if the goal permits).
 
 Apart from this, there are the following introduction patterns that can only