From 4f918d4a1f5e67bb42c689233a21601fc31cd2f7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 1 Jul 2016 01:21:20 +0200
Subject: [PATCH] Tweak tests/one_shot.

---
 tests/one_shot.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/one_shot.v b/tests/one_shot.v
index 768662ea3..6cd421733 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -52,11 +52,11 @@ 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].
+    + 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".
-    + wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight.
+    + wp_cas_fail. rewrite /one_shot_inv; eauto 10.
   - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
     iAssert (∃ v, l ↦ v ★ ((v = InjLV #0 ★ own γ Pending) ∨
        ∃ n : Z, v = InjRV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "Hv".
-- 
GitLab