From e127094f8a2ffbf327b80aa175ef51e1af98dcb1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Feb 2019 12:40:21 +0100
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/lifetime/model/borrow_sep.v | 4 ++--
theories/lifetime/model/definitions.v | 2 +-
theories/lifetime/model/primitive.v | 4 ++--
theories/lifetime/model/reborrow.v | 4 ++--
5 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/opam b/opam
index 3830f036..5bcd9528 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
- "coq-iris" { (= "dev.2019-02-20.0.8a8c1405") | (= "dev") }
+ "coq-iris" { (= "dev.2019-02-21.1.ef511c16") | (= "dev") }
]
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 60be506b..45ba12f1 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -78,9 +78,9 @@ Proof.
iIntros (?) "#LFT HP HQ". rewrite {1 2}/bor.
iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "Hbor1".
- done. by apply gmultiset_union_subseteq_l.
+ done. by apply gmultiset_disj_union_subseteq_l.
iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "Hbor2".
- done. by apply gmultiset_union_subseteq_r.
+ done. by apply gmultiset_disj_union_subseteq_r.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
iDestruct "Hslice1" as (P') "[#HPP' Hslice1]".
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 580275ad..ae52a295 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -17,7 +17,7 @@ Module Export lft_notation.
End lft_notation.
Definition static : lft := (∅ : gmultiset _).
-Definition lft_intersect (κ κ' : lft) : lft := κ ∪ κ'.
+Definition lft_intersect (κ κ' : lft) : lft := κ ⊎ κ'.
Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 25519cbb..19ca418d 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -221,7 +221,7 @@ Proof. exists Λ. by rewrite lookup_insert. Qed.
Lemma lft_dead_in_alive_in_union A κ κ' :
lft_dead_in A (κ ⊓ κ') → lft_alive_in A κ → lft_dead_in A κ'.
Proof.
- intros (Λ & [Hin|Hin]%elem_of_union & HΛ) Halive.
+ intros (Λ & [Hin|Hin]%gmultiset_elem_of_disj_union & HΛ) Halive.
- contradict HΛ. rewrite (Halive _ Hin). done.
- exists Λ. auto.
Qed.
@@ -264,7 +264,7 @@ Instance lft_intersect_left_id : LeftId eq static lft_intersect := _.
Instance lft_intersect_right_id : RightId eq static lft_intersect := _.
Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
-Proof. by rewrite /lft_tok -big_sepMS_union. Qed.
+Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed.
Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2].
Proof.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index e7500c0f..b0c84dd1 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -173,9 +173,9 @@ Proof.
rewrite /idx_bor /bor. destruct i as [κ0 i].
iDestruct "HP" as "[Hκκ0 HP]". iDestruct "HP" as (P') "[HPP' HP']".
iMod (raw_bor_shorten _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "Hbor";
- [done|by apply gmultiset_union_subseteq_r|].
+ [done|by apply gmultiset_disj_union_subseteq_r|].
iMod (raw_idx_bor_unnest with "LFT HP' Hbor") as "Hbor";
- [done|by apply gmultiset_union_subset_l|].
+ [done|by apply gmultiset_disj_union_subset_l|].
iExists _. iDestruct (raw_bor_iff with "HPP' Hbor") as "$".
by iApply lft_intersect_mono.
Qed.
--
GitLab