From 6d66d9d143d3675664a24873cb0bcb5803720629 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 20 Nov 2016 15:54:06 +0100
Subject: [PATCH] =?UTF-8?q?Support=20=E2=96=A0=20(=E2=88=80=20=5F,=20=5F)?=
 =?UTF-8?q?=20and=20=E2=96=A0=20(=5F=20=E2=86=92=20=5F)=20in=20iIntros.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 proofmode/coq_tactics.v | 7 +++++++
 proofmode/tactics.v     | 4 +++-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 3eb34c8f3..ae4628e67 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -475,6 +475,9 @@ Proof.
   intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
   by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
 Qed.
+Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
+  (φ → Δ ⊢ ■ ψ) → Δ ⊢ ■ (φ → ψ).
+Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
 Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
@@ -777,6 +780,10 @@ Qed.
 Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ ⊢ ∀ a, Φ a.
 Proof. apply forall_intro. Qed.
 
+Lemma tac_pure_forall_intro {A} Δ (φ : A → Prop) :
+  (∀ a, Δ ⊢ ■ φ a) → Δ ⊢ ■ ∀ a, φ a.
+Proof. intros. rewrite pure_forall. by apply forall_intro. Qed.
+
 Class ForallSpecialize {As} (xs : hlist As)
   (P : uPred M) (Φ : himpl As (uPred M)) := forall_specialize : P ⊢ Φ xs.
 Arguments forall_specialize {_} _ _ _ {_}.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index bd49ad159..831e049dd 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -684,7 +684,9 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
        apply _ || fail "iIntro:" P "not pure"|]
     |(* (?P -∗ _) *) eapply tac_wand_intro_pure;
       [let P := match goal with |- IntoPure ?P _ => P end in
-       apply _ || fail "iIntro:" P "not pure"|]];
+       apply _ || fail "iIntro:" P "not pure"|]
+    |(* (■ ∀ _, _) *) apply tac_pure_forall_intro
+    |(* (■ (_ → _)) *) apply tac_pure_impl_intro];
   intros x.
 
 Local Tactic Notation "iIntro" constr(H) := first
-- 
GitLab