From f400f576ea7e294c159b6726ff8fb5bd9d05893f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 Jun 2016 13:46:37 +0200
Subject: [PATCH] Create eauto hint for iPvsIntro.

---
 proofmode/pviewshifts.v | 3 +++
 tests/one_shot.v        | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 013403208..20de4de2e 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -181,3 +181,6 @@ Tactic Notation "iTimeless" constr(H) :=
 
 Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
   iTimeless H; iDestruct H as Hs.
+
+Hint Extern 2 (of_envs _ ⊢ _) =>
+  match goal with |- _ ⊢ (|={_}=> _)%I => iPvsIntro end.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 31b1b2bbd..768662ea3 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -52,7 +52,7 @@ Proof.
   iPvsIntro. iApply "Hf"; iSplit.
   - iIntros {n} "!". wp_let.
     iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
-    + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft; iPvsIntro].
+    + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft].
       iPvs (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Cinr (DecAgree n)). }
       iPvsIntro; iRight; iExists n; by iSplitL "Hl".
@@ -79,7 +79,7 @@ Proof.
     iCombine "Hγ" "Hγ'" as "Hγ".
     iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
     iSplitL "Hl"; [iRight; by eauto|].
-    wp_match. iApply wp_assert'. wp_op=>?; iPvsIntro; simplify_eq/=; eauto.
+    wp_match. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
 Qed.
 
 Lemma hoare_one_shot (Φ : val → iProp) :
-- 
GitLab