From a71965c47fced41c1150656ca2a92cab0e78e25a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 24 Aug 2017 09:28:34 +0200
Subject: [PATCH] Fix issue #95.

---
 theories/proofmode/coq_tactics.v | 9 ++++++---
 theories/proofmode/tactics.v     | 6 ++++--
 theories/tests/proofmode.v       | 3 +++
 3 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 732bbb149..71e728e6f 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -492,12 +492,15 @@ Qed.
 
 (** * Implication and wand *)
 Lemma tac_impl_intro Δ Δ' i P Q :
-  env_spatial_is_nil Δ = true →
+  (if env_spatial_is_nil Δ then Unit else PersistentP P) →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
-  intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
-  by rewrite right_id always_wand_impl always_elim HQ.
+  intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
+  - rewrite (persistentP Δ) envs_app_sound //; simpl.
+    by rewrite right_id always_wand_impl always_elim.
+  - apply impl_intro_l. rewrite envs_app_sound //; simpl.
+    by rewrite always_and_sep_l right_id wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   IntoPersistentP P P' →
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 15dc96e15..890a1e6b0 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -299,8 +299,10 @@ Local Tactic Notation "iIntro" constr(H) :=
   first
   [ (* (?Q → _) *)
     eapply tac_impl_intro with _ H; (* (i:=H) *)
-      [reflexivity || fail 1 "iIntro: introducing" H
-                             "into non-empty spatial context"
+      [env_cbv; apply _ ||
+       let P := lazymatch goal with |- PersistentP ?P => P end in
+       fail 1 "iIntro: introducing non-persistent" H ":" P
+              "into non-empty spatial context"
       |env_reflexivity || fail "iIntro:" H "not fresh"
       |]
   | (* (_ -∗ _) *)
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index c162461d7..5208ff9e7 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -77,6 +77,9 @@ Proof.
   done.
 Qed.
 
+Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P → Q → P ∗ Q)%I.
+Proof. iIntros "H1 H2". by iFrame. Qed.
+
 Lemma test_fast_iIntros P Q :
   (∀ x y z : nat,
     ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x))%I.
-- 
GitLab