From a4e7cd6b31e822372362497d020b74348ab4ec32 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 26 Feb 2020 11:59:34 +0100
Subject: [PATCH] bump Iris, adjust for TCEq changes
---
opam | 2 +-
theories/typing/lib/mutex/mutexguard.v | 2 +-
theories/typing/lib/rc/rc.v | 4 ++--
theories/typing/lib/refcell/refmut_code.v | 4 ++--
theories/typing/lib/rwlock/rwlockreadguard_code.v | 2 +-
theories/typing/lib/rwlock/rwlockwriteguard_code.v | 2 +-
theories/typing/programs.v | 2 +-
7 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/opam b/opam
index 50566837..eb3bb013 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2020-02-25.0.55283d57") | (= "dev") }
+ "coq-iris" { (= "dev.2020-02-25.3.bb9152ec") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 17705ae9..1f30e5f0 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -252,7 +252,7 @@ Section code.
[solve_typing..|].
iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hclose4]".
wp_bind (!_)%E. iApply (wp_step_fupd with "[Hshr Hα2β]");
- [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+ [|by iApply ("Hshr" with "[] Hα2β")|]; first done.
wp_read. iIntros "[#Hshr Hα2β] !>". wp_let.
iDestruct ("Hclose4" with "Hα2β") as "[Hβ Hα2]".
iMod ("Hclose3" with "Hβ HL") as "HL".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 654a10db..03e65d8a 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -695,7 +695,7 @@ Section code.
- subst strong. wp_op. wp_if. wp_op.
rewrite shift_loc_0. wp_write. wp_bind (#☠;;#☠)%E.
iApply (wp_step_fupd with "[Hproto Hrc]");
- [| |by iApply ("Hproto" with "Hrc")|];
+ [|by iApply ("Hproto" with "Hrc")|];
[done..|wp_seq; iIntros "(Hty&H†&Hna&Hproto) !>"].
rewrite <-freeable_sz_full_S, <-(freeable_sz_split _ 2 ty.(ty_size)).
iDestruct "H†" as "[H†1 H†2]". wp_seq. wp_bind (_<-_;;_)%E.
@@ -790,7 +790,7 @@ Section code.
iDestruct "Hc" as "[[% [_ Hproto]]|[% [_ Hproto]]]".
- subst strong. wp_bind (#1 = #1)%E.
iApply (wp_step_fupd with "[Hproto Hrc]");
- [| |by iApply ("Hproto" with "Hrc")|];
+ [|by iApply ("Hproto" with "Hrc")|];
[done..|wp_op; iIntros "(Hty&H†&Hna&Hproto) !>"; wp_if].
rewrite <-freeable_sz_full_S, <-(freeable_sz_split _ 2 ty.(ty_size)).
iDestruct "H†" as "[H†1 H†2]". wp_bind (_<-_;;_)%E.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index ae82ed43..c9b45260 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -36,7 +36,7 @@ Section refmut_functions.
[solve_typing..|].
iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
wp_bind (!#lx')%E. iApply (wp_step_fupd with "[Hα2β]");
- [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+ [|by iApply ("Hshr" with "[] Hα2β")|]; first done.
iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β] !>". wp_let.
iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
@@ -152,7 +152,7 @@ Section refmut_functions.
iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
rewrite assoc (comm _ q'' q) //. }
wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done.
- iApply (wp_step_fupd with "INV"); [done|set_solver|]. wp_seq. iIntros "{Hb} Hb !>".
+ iApply (wp_step_fupd with "INV"); [set_solver|]. wp_seq. iIntros "{Hb} Hb !>".
iMod ("Hcloseβ" with "Hb Hna") as "[Hβ Hna]".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
iApply (type_type _ _ _ [ #lx â— box (uninit 2)]
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 2cb00ca6..b1a160c9 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -119,7 +119,7 @@ Section rwlockreadguard_functions.
{ rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
rewrite {1}EQn -{1}(agree_idemp (to_agree _)) 2!pair_op Cinr_op Some_op.
apply (cancel_local_update_unit (reading_st q ν)) , _. }
- iApply (wp_step_fupd with "INV"). done. set_solver.
+ iApply (wp_step_fupd with "INV"). set_solver.
iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 0646d740..45c9edd7 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -37,7 +37,7 @@ Section rwlockwriteguard_functions.
[solve_typing..|].
iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hα2β]");
- [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+ [|by iApply ("Hshr" with "[] Hα2β")|]; first done.
iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_op. wp_let.
iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1". iMod ("Hclose'" with "Hβ HL") as "HL".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index a5bea9a8..56e7e825 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -168,7 +168,7 @@ Section typing_rules.
iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
iApply (wp_mask_mono _ (↑lftN)); first done.
- iApply (wp_step_fupd with "Hend"). done. set_solver. wp_seq.
+ iApply (wp_step_fupd with "Hend"); first set_solver. wp_seq.
iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
Qed.
--
GitLab