Let iAlways clear spatial context.

This fixes issue #81.

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.

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' →

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.