From bc4b0cc2544d9f94524ef7e2bad2b5667d0e5b84 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 5 Mar 2017 21:40:02 +0100
Subject: [PATCH] Strong framing by default for persistent hypotheses.

---
 theories/proofmode/tactics.v | 13 +++++++++----
 theories/tests/proofmode.v   | 10 +++++-----
 2 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index b59d72dcd..a709ea663 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -182,14 +182,19 @@ Local Ltac iFramePure t :=
     |iFrameFinish].
 
 Local Ltac iFrameHyp strong H :=
-  eapply tac_frame with _ H _ _ _;
-    [env_cbv; reflexivity || fail "iFrame:" H "not found"
+  (* Create an evar so we can remember whether the hypothesis is persistent. If
+  it is, we won't drop the hypothesis anyway, so we can use strong framing
+  safely. *)
+  let q := fresh in evar (q : bool);
+  eapply tac_frame with _ H q _ _;
+    [env_cbv; apply: reflexivity (* reflexivity fails because of the evar *)
+      || fail "iFrame:" H "not found"
     |let R := match goal with |- Frame ?R _ _ => R end in
-     lazymatch strong with
+     lazymatch eval compute in (q || strong) with
      | false => apply _
      | true => typeclasses eauto with typeclass_instances strong_frame
      end || fail "iFrame: cannot frame" R
-    |iFrameFinish].
+    |unfold q; clear q; iFrameFinish].
 
 Local Ltac iFrameAnyPure :=
   repeat match goal with H : _ |- _ => iFramePure H end.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index e0258386a..c62f348c2 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -147,10 +147,10 @@ Lemma demo_17 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
 
-Lemma demo_18 (M : ucmraT) (P Q R : uPred M) :
-  P -∗ Q -∗ R -∗ (P ∗ Q ∨ R ∗ False).
+Lemma demo_18 (M : ucmraT) (P Q Q2 R : uPred M) `{!PersistentP Q2}:
+  P -∗ Q -∗ Q2 -∗ R -∗ (P ∗ Q ∗ Q2 ∨ R ∗ False).
 Proof.
-  iIntros "^$ HQ HR {^$HR}".
-  iAssert (Q ∨ False)%I with "[^$HQ]" as "[HQ|[]]".
-  iFrame "^HQ".
+  iIntros "^$ HQ1 #HQ2 HR {^$HR}".
+  iAssert (Q ∨ False)%I with "[^$HQ1]" as "[HQ1|[]]".
+  iFrame "^HQ1 HQ2".
 Qed.
-- 
GitLab