From a38a1915d3c4eaa897b114f19406e2b74ae40a4b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2021 13:54:08 +0100
Subject: [PATCH] update dependencies
---
coq-lambda-rust.opam | 2 +-
theories/lifetime/model/accessors.v | 4 ++--
theories/lifetime/model/in_at_borrow.v | 2 +-
theories/typing/lib/arc.v | 12 ++++++------
theories/typing/util.v | 4 ++--
5 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 784eb2ce..85519abd 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2021-02-14.0.24c31b61") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2021-02-16.0.c0f38bcc") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 3073b4d2..ce7933d4 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -347,7 +347,7 @@ Proof.
- iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iExists _. iFrame "%". iRight. by iFrame.
- iExists (i.1). rewrite monPred_subjectively_unfold /=. iFrame "#".
- rewrite bi.True_emp. iApply fupd_intro_mask'. solve_ndisj. }
+ rewrite bi.True_emp. iApply fupd_mask_subseteq. solve_ndisj. }
iLeft. unfold lft_bor_alive, idx_bor_own. iDestruct "Hbor" as (Vb) "[#HVb Hbor]".
iExists (P' Vb), (i.1). iFrame "#". rewrite [in _ Vκ]lft_inv_alive_unfold /lft_bor_alive.
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
@@ -358,7 +358,7 @@ Proof.
solve_ndisj. by rewrite lookup_fmap EQB.
iApply fupd_frame_l. iSplitL "HP'".
{ iNext. iSplit; [done|]. iApply "HPP'". by iApply monPred_in_elim. }
- iMod fupd_intro_mask' as "Hclose"; [|iModIntro; iIntros (Q) "HvsQ HQ"].
+ iMod fupd_mask_subseteq as "Hclose"; [|iModIntro; iIntros (Q) "HvsQ HQ"].
solve_ndisj.
iMod "Hclose" as "_".
iAssert (▷⌜Vb ⊑ Vκ⌝)%I as "#>%".
diff --git a/theories/lifetime/model/in_at_borrow.v b/theories/lifetime/model/in_at_borrow.v
index a32326e8..cc7eb365 100644
--- a/theories/lifetime/model/in_at_borrow.v
+++ b/theories/lifetime/model/in_at_borrow.v
@@ -62,7 +62,7 @@ Proof.
iDestruct (monPred_in_intro with "Htok") as (V) "[#HV Htok]".
iMod (idx_bor_acc_internal with "LFT Hs Hown Htok") as (Vb) "(% & HP & Hclose'')".
solve_ndisj. solve_ndisj.
- iMod fupd_intro_mask' as "Hclose'''"; last iModIntro. solve_ndisj.
+ iMod fupd_mask_subseteq as "Hclose'''"; last iModIntro. solve_ndisj.
iExists Vb. iSplitL "HP".
{ iIntros "HVb". iApply "HPP'". iApply (monPred_in_elim with "HVb").
by rewrite monPred_at_later. }
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index b17b655c..40a7f345 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -563,7 +563,7 @@ Section arc.
first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
- iExists Vb, q'. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
+ iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
@@ -609,7 +609,7 @@ Section arc.
with "[] [] WR [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
- iExists Vb, q'. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
+ iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj. iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
@@ -658,7 +658,7 @@ Section arc.
[by iDestruct "Hpersist" as "[$ _]"| |by iExists _,_|].
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
- iExists Vb, q'. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
+ iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj. iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (t'' q'') "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
@@ -707,7 +707,7 @@ Section arc.
[by iDestruct "Hpersist" as "[$ _]"| |by iExists _,_|].
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
- iExists Vb, q'. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
+ iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj. iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (??) "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
@@ -754,7 +754,7 @@ Section arc.
with "[] [] WR [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
- iExists Vb, q'. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
+ iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj. iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (??) "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
@@ -805,7 +805,7 @@ Section arc.
[by iDestruct "Hpersist" as "[$ _]"| |by iExists _,_|].
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
- iExists Vb, q0. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
+ iExists Vb, q0. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj. iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros ([] q') "[Hα Hown]"; wp_if; iMod ("Hclose1" with "Hα HL") as "HL".
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 6cbb1e3b..e9c5350c 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -47,7 +47,7 @@ Section util.
iModIntro. iNext. iMod "Hdelay" as "[Hb Htok]".
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; first solve_ndisj.
iApply "Hclose". auto.
- - iMod fupd_intro_mask' as "Hclose'"; first solve_ndisj. iModIntro.
+ - iMod fupd_mask_subseteq as "Hclose'"; first solve_ndisj. iModIntro.
iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_".
+ iModIntro. eauto.
+ iFrame. iModIntro. by iApply monPred_in_elim.
@@ -79,7 +79,7 @@ Section util.
iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]"; first solve_ndisj.
{ by iApply bor_shorten. }
iMod ("Hclose" with "[]") as "_"; auto.
- - iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first solve_ndisj.
+ - iMod fupd_mask_subseteq as "Hclose'"; last iModIntro; first solve_ndisj.
iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_".
+ iModIntro. eauto.
+ iFrame. iModIntro. by iApply monPred_in_elim.
--
GitLab