From 124eea15dc24e75c06b469693f833647839c889c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Mar 2017 21:11:01 +0100
Subject: [PATCH] Let iAlways clear spatial context.

This fixes issue #81.
---
 ProofMode.md                     | 2 +-
 theories/proofmode/coq_tactics.v | 8 ++++++--
 theories/proofmode/tactics.v     | 5 ++---
 3 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 2071dd351..773baa3ff 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 28cd29420..66591afe5 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 15c121dcb..d12e7d4d9 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.
-- 
GitLab