From 2050c2e19800471700d4095257a46a4231508cf9 Mon Sep 17 00:00:00 2001
From: Zhen Zhang <izgzhen@gmail.com>
Date: Thu, 22 Dec 2016 20:59:59 +0800
Subject: [PATCH] Move f_spec back to peritem

---
 theories/flat.v    | 7 +------
 theories/peritem.v | 6 ++++++
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/theories/flat.v b/theories/flat.v
index 9850ce9..07b98eb 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -130,13 +130,8 @@ Section proof.
     iFrame. iFrame "#".
   Qed.
 
-  Definition f_spec (R: iProp Σ) (f: val) (Rf: iProp Σ) x :=
-    {{{ inv N R ∗ Rf }}}
-      f x
-    {{{ RET #(); Rf }}}.
-
   Lemma doOp_f_spec R γm γr (p: loc) ts:
-    f_spec (p_inv R γm γr ts p) doOp (own γr (Excl ()) ∗ R)%I #p.
+    f_spec N (p_inv R γm γr ts p) doOp (own γr (Excl ()) ∗ R)%I #p.
   Proof.
     iIntros (Φ) "(#H1 & Hor & HR) HΦ".
     wp_rec. wp_bind (! _)%E.
diff --git a/theories/peritem.v b/theories/peritem.v
index dee70a5..76a54ad 100644
--- a/theories/peritem.v
+++ b/theories/peritem.v
@@ -30,6 +30,12 @@ Section defs.
       iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
       iModIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
   Qed.
+
+  Definition f_spec (R: iProp Σ) (f: val) (Rf: iProp Σ) x :=
+    {{{ inv N R ∗ Rf }}}
+      f x
+    {{{ RET #(); Rf }}}.
+
 End defs.
 
 Section proofs.
-- 
GitLab