diff --git a/ProofMode.md b/ProofMode.md
index d178f52f0abc8ca80f3c8cb45949df86ea59cb22..2eaab453a1c2a5c648f7c07723e9de89ebbb18f4 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -188,8 +188,13 @@ _introduction patterns_:
 - `?` : create an anonymous hypothesis.
 - `_` : remove the hypothesis.
 - `$` : frame the hypothesis in the goal.
-- `[ipat ipat]` : (separating) conjunction elimination.
-- `[ipat|ipat]` : disjunction elimination.
+- `[ipat1 ipat2]` : (separating) conjunction elimination. In order to eliminate
+  conjunctions `P ∧ Q` in the spatial context, one of the following conditions
+  should hold:
+  + Either the proposition `P` or `Q` should be persistent.
+  + Either `ipat1` or `ipat2` should be `_`, which results in one of the
+    conjuncts to be thrown away.
+- `[ipat1|ipat2]` : disjunction elimination.
 - `[]` : false elimination.
 - `%` : move the hypothesis to the pure Coq context (anonymously).
 - `# ipat` : move the hypothesis to the persistent context.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 53c6708799b3287ed165dee9e084afb34f36c956..57d935317b6b0e49ed5c3dcd8cf751d5ae5a38b5 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -778,7 +778,8 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Always *)
 Tactic Notation "iAlways":=
   iStartProof;
-  apply tac_always_intro; env_cbv.
+  apply tac_always_intro; env_cbv
+    || fail "iAlways: the goal is not an always modality".
 
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=