From 99703f4498cdfd69b86139db460f93741f4d4b24 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 16 Oct 2016 23:21:33 +0200
Subject: [PATCH] Update wrt iris.
---
adequacy.v | 1 -
heap.v | 10 +++++-----
lifting.v | 2 +-
races.v | 2 +-
4 files changed, 7 insertions(+), 8 deletions(-)
diff --git a/adequacy.v b/adequacy.v
index 113067d4..27f33157 100644
--- a/adequacy.v
+++ b/adequacy.v
@@ -1,7 +1,6 @@
From iris.program_logic Require Export weakestpre adequacy.
From lrust Require Export heap.
From iris.algebra Require Import auth.
-From iris.program_logic Require Import ownership.
From lrust Require Import proofmode notation.
Class heapPreG Σ := HeapPreG {
diff --git a/heap.v b/heap.v
index 00f8240d..cf583bec 100644
--- a/heap.v
+++ b/heap.v
@@ -1,6 +1,6 @@
From iris.algebra Require Import upred_big_op cmra_big_op gmap frac dec_agree.
From iris.algebra Require Import csum excl auth.
-From iris.program_logic Require Export invariants ownership.
+From iris.program_logic Require Export invariants wsat.
From iris.proofmode Require Export tactics.
From lrust Require Export lifting.
Import uPred.
@@ -468,8 +468,8 @@ Section heap.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
iVs (heap_read_vs _ 0 1 with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iApply pvs_intro'; [set_solver|iIntros "Hclose'"].
- iExists σ, n, v. iFrame. iSplit; [done|]. iIntros "!> Hσ".
+ iVs (pvs_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
+ iVsIntro. iExists σ, n, v. iFrame. iSplit; [done|]. iIntros "!> Hσ".
iVs "Hclose'" as "_". iVs ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
{ iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
iVsIntro. clear dependent n σ hF.
@@ -519,8 +519,8 @@ Section heap.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
iVs (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iApply pvs_intro'; [set_solver|iIntros "Hclose'"].
- iExists σ, v'. iSplit; [done|]. iIntros "{$Hσ} !> Hσ".
+ iVs (pvs_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
+ iVsIntro. iExists σ, v'. iSplit; [done|]. iIntros "{$Hσ} !> Hσ".
iVs "Hclose'" as "_". iVs ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
{ iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
iVsIntro. clear dependent σ hF.
diff --git a/lifting.v b/lifting.v
index 8373138c..e6d8d180 100644
--- a/lifting.v
+++ b/lifting.v
@@ -1,5 +1,5 @@
From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
+From iris.program_logic Require Import ectx_lifting wsat. (* for ownP *)
From lrust Require Export lang.
From lrust Require Import tactics.
From iris.proofmode Require Import tactics.
diff --git a/races.v b/races.v
index 32cf4acd..c7273d30 100644
--- a/races.v
+++ b/races.v
@@ -1,5 +1,5 @@
From iris.program_logic Require Export hoare.
-From iris.program_logic Require Import ownership adequacy.
+From iris.program_logic Require Import adequacy.
From lrust Require Import tactics.
From iris.prelude Require Import gmap.
--
GitLab