From 25f6e91646d3465d760dd369e1bdf25c94b79097 Mon Sep 17 00:00:00 2001
From: Zhen Zhang <izgzhen@gmail.com>
Date: Wed, 24 Aug 2016 13:14:32 +0200
Subject: [PATCH] Fix FIXME in atomic.v

---
 tests/atomic.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/tests/atomic.v b/tests/atomic.v
index 8bf295082..7958526f7 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -61,19 +61,16 @@ Section demo.
     wp_load.
     iVs ("Hvs'" with "Hl") as "HP".
     iVsIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
-    (* iVs ("Hvs" with "HP") as (x) "[Hl Hvs']". (* FIXME: Can't apply, bug? *) *)
-    iApply (wp_atomic ⊤ heapN _); first by solve_atomic.
     iVs ("Hvs" with "HP") as (x') "[Hl Hvs']".
     destruct (decide (x = x')).
     - subst.
       iDestruct "Hvs'" as "[_ Hvs']".
       iSpecialize ("Hvs'" $! #x').
-      iVsIntro.
       wp_cas_suc.
       iVs ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
       iVsIntro. wp_if. iVsIntro. by iExists x'.
     - iDestruct "Hvs'" as "[Hvs' _]".
-      iVsIntro. wp_cas_fail.
+      wp_cas_fail.
       iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
       iVsIntro. wp_if. by iApply "IH".
   Qed.
-- 
GitLab