diff --git a/ProofMode.md b/ProofMode.md
index 2071dd3512d1aa4b5c806652b0b24d2e0dbc51cb..773baa3fff414ee1212212d4942f3ef9ee76b3c9 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -200,7 +200,7 @@ appear at the top level:
 - `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
   previous pattern, e.g., `{$H1 H2 $H3}`).
 - `!%` : introduce a pure goal (and leave the proof mode).
-- `!#` : introduce an always modality (given that the spatial context is empty).
+- `!#` : introduce an always modality and clear the spatial context.
 - `!>` : introduce a modality.
 - `/=` : perform `simpl`.
 - `//` : perform `try done` on all goals.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 28cd294202e2f071c765ab8859fa924f4c489e92..66591afe5e4d0edb7506dbadcab4c9e40a9e444f 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -474,8 +474,12 @@ Proof.
 Qed.
 
 (** * Always *)
-Lemma tac_always_intro Δ Q : env_spatial_is_nil Δ = true → (Δ ⊢ Q) → Δ ⊢ □ Q.
-Proof. intros. by apply (always_intro _ _). Qed.
+Lemma tac_always_intro Δ Q :
+  (envs_clear_spatial Δ ⊢ Q) → Δ ⊢ □ Q.
+Proof.
+  intros <-. rewrite envs_clear_spatial_sound sep_elim_l.
+  by apply (always_intro _ _).
+Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) → IntoPersistentP P P' →
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 15c121dcbd467aacf3ad6f26594a4edb357ee3cb..d12e7d4d9b98dd963faac79303e91b8ab48e0727 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -779,8 +779,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Always *)
 Tactic Notation "iAlways":=
   iStartProof;
-  apply tac_always_intro;
-    [reflexivity || fail "iAlways: spatial context non-empty"|].
+  apply tac_always_intro; env_cbv.
 
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
@@ -1518,7 +1517,7 @@ Hint Extern 0 (_ ⊢ _) => progress iIntros.
 Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
-Hint Extern 1 (of_envs _ ⊢ □ _) => iClear "*"; iAlways.
+Hint Extern 1 (of_envs _ ⊢ □ _) => iAlways.
 Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
 Hint Extern 1 (of_envs _ ⊢ |==> _) => iModIntro.
 Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.