Fix always

d0830956 · Zhen Zhang · 9ce6b20e · d0830956 · d0830956 · d0830956
Commit d0830956 authored Oct 12, 2016 by Zhen Zhang
Hide whitespace changes
Inline Side-by-side

Showing with 7 additions and 7 deletions

IRIS_VERSION IRIS_VERSION +1 -1

flat.v flat.v +1 -1

misc.v misc.v +3 -3

simple_sync.v simple_sync.v +1 -1

sync.v sync.v +1 -1

No files found.
--- a/IRIS_VERSION
+++ b/IRIS_VERSION
-9c5a95d3b271f4e0d0c657964dfa386070d0b322
+a0fc612e5c81bbff25f63938b50f448ecc056c68
--- a/flat.v
+++ b/flat.v
@@ -405,7 +405,7 @@ Section proof.
    iFrame "Hh Hm". iIntros (γ s) "#Hss".
    wp_let. iVsIntro. iApply "HΦ". rewrite /synced.
    iAlways.
-    iIntros (f). wp_let. iVsIntro. iAlways.
+    iIntros (f). wp_let. iVsIntro.
    iIntros (P Q x) "#Hf".
    iIntros "!# Hp". wp_let.
    wp_bind (install _ _ _).

--- a/misc.v
+++ b/misc.v
@@ -3,6 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import auth frac gmap dec_agree upred_big_op.
 From iris.prelude Require Import countable.
+From iris.program_logic Require Import auth.
 Import uPred.

 Section lemmas.
@@ -59,10 +60,10 @@ Section heap_extra.
    iIntros (?) "(#Hh & Hp1 & Hp2)".
    iCombine "Hp1" "Hp2" as "Hp".
    iDestruct (heap_mapsto_op_1 with "Hp") as "[_ Hp]".
-    rewrite heap_mapsto_eq. iDestruct (own_valid with "Hp") as %H'.
+    rewrite heap_mapsto_eq. iDestruct (auth_own_valid with "Hp") as %H'.    
    apply singleton_valid in H'. by destruct H' as [H' _].
  Qed.
-  
+
 End heap_extra.

 Section big_op_later.
@@ -106,4 +107,3 @@ Section pair.
    rewrite pair_op frac_op' dec_agree_idemp. by iFrame.
  Qed.
 End pair.
-
--- a/simple_sync.v
+++ b/simple_sync.v
@@ -28,7 +28,7 @@ Section syncer.
    iSplitR "HR HΦ"; first done.
    iFrame "HR".
    iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
-    iIntros (f). wp_let. iVsIntro. iAlways.
+    iIntros (f). wp_let. iVsIntro.
    iIntros (P Q x) "#Hf !# HP".
    wp_let. wp_bind (acquire _).
    iApply acquire_spec. iSplit; first done.

--- a/sync.v
+++ b/sync.v
@@ -6,7 +6,7 @@ Section sync.
  Context `{!heapG Σ} (N : namespace).
  
  Definition synced R (f' f: val) :=
-    (□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) → ({{ P x }} f' x {{ v, Q x v }}))%I.
+    (∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) → ({{ P x }} f' x {{ v, Q x v }}))%I.

  Definition is_syncer (R: iProp Σ) (s: val) :=
    (∀ (f : val), WP s f {{ f', synced R f' f }})%I.