From 19e03d377fa67c2f1bba81e0bb9b9e5b6be31d13 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Feb 2018 19:35:47 +0100
Subject: [PATCH] Fix regression caused by
 0b46262075b1177750922d902af84c877a7b3197.

This regression was caused by a bug in handling spec patterns.
---
 theories/proofmode/coq_tactics.v | 10 ++++++++++
 theories/proofmode/tactics.v     |  4 +++-
 theories/tests/proofmode.v       |  5 +++++
 3 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 43731e08d..a34a4aab1 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -900,6 +900,16 @@ Proof.
        (into_persistent _ R) sep_elim_r persistently_and_affinely_sep_l wand_elim_r.
 Qed.
 
+(* A special version of [tac_assumption] that does not do any of the
+[FromAssumption] magic. *)
+Lemma tac_specialize_persistent_helper_done Δ i q P :
+  envs_lookup i Δ = Some (q,P) →
+  envs_entails Δ (bi_absorbingly P).
+Proof.
+  rewrite envs_entails_eq /bi_absorbingly=> /envs_lookup_sound=> ->.
+  rewrite affinely_persistently_if_elim comm. f_equiv; auto.
+Qed.
+
 Lemma tac_revert Δ Δ' i p P Q :
   envs_lookup_delete true i Δ = Some (p,P,Δ') →
   envs_entails Δ' ((if p then □ P else P)%I -∗ Q) →
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index b2824988e..458b50756 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -615,7 +615,9 @@ Tactic Notation "iSpecializeCore" open_constr(H)
        (* FIXME: do something reasonable when the BI is not affine *)
        eapply tac_specialize_persistent_helper with _ H _ _ _ _;
          [env_reflexivity || fail "iSpecialize:" H "not found"
-         |iSpecializePat H pat; last (iExact H)
+         |iSpecializePat H pat;
+           [..
+           |eapply tac_specialize_persistent_helper_done with H _; env_reflexivity]
          |apply _ ||
           let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
           fail "iSpecialize:" Q "not persistent"
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index e43121200..040a0a430 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -94,6 +94,11 @@ Proof.
   done.
 Qed.
 
+Lemma test_iAssert_persistently P : □ P -∗ True.
+Proof.
+  iIntros "HP". iAssert (â–¡ P)%I with "[# //]" as "#H". done.
+Qed.
+
 Lemma test_iSpecialize_auto_frame P Q R :
   (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
 Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
-- 
GitLab