From 26b62a4bf460094924cb7f79cf9db9680bf28f3f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 19 Sep 2019 18:01:06 +0200
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/lang/heap.v | 2 +-
theories/lang/lang.v | 4 ++--
theories/lifetime/lifetime_sig.v | 4 ++--
theories/lifetime/model/creation.v | 6 +++---
theories/lifetime/model/definitions.v | 2 +-
theories/lifetime/model/primitive.v | 4 ++--
theories/typing/lft_contexts.v | 2 +-
theories/typing/type.v | 6 +++---
9 files changed, 16 insertions(+), 16 deletions(-)
diff --git a/opam b/opam
index 272902f3..0ffbd247 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-09-19.0.ca3f9d11") | (= "dev") }
+ "coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index d7ec2614..4abef3c1 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -174,7 +174,7 @@ Section heap.
{ rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
iDestruct (IH (l +ₗ 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
- rewrite (inj_iff (:: vl2)).
+ rewrite (inj_iff (.:: vl2)).
iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
iSplit; first done. iFrame.
- by iIntros "[% [$ Hl2]]"; subst.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 6ce23b84..06af6e4e 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -430,13 +430,13 @@ Qed.
Definition fresh_block (σ : state) : block :=
let loclst : list loc := elements (dom _ σ : gset loc) in
- let blockset : gset block := foldr (λ l, ({[l.1]} ∪)) ∅ loclst in
+ let blockset : gset block := foldr (λ l, ({[l.1]} ∪.)) ∅ loclst in
fresh blockset.
Lemma is_fresh_block σ i : σ !! (fresh_block σ,i) = None.
Proof.
assert (∀ (l : loc) ls (X : gset block),
- l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪)) X ls) as help.
+ l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪.)) X ls) as help.
{ induction 1; set_solver. }
rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
move=> /(help _ _ ∅) /=. apply is_fresh.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 77311728..10a29398 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -54,8 +54,8 @@ Module Type lifetime_sig.
Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓).
Global Declare Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓).
- Global Declare Instance lft_intersect_inj_1 (κ : lft) : Inj eq eq (κ ⊓).
- Global Declare Instance lft_intersect_inj_2 (κ : lft) : Inj eq eq (⊓ κ).
+ Global Declare Instance lft_intersect_inj_1 (κ : lft) : Inj eq eq (κ ⊓.).
+ Global Declare Instance lft_intersect_inj_2 (κ : lft) : Inj eq eq (.⊓ κ).
Global Declare Instance lft_intersect_left_id : LeftId eq static meet.
Global Declare Instance lft_intersect_right_id : RightId eq static meet.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 72ed9049..e0862b40 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -36,14 +36,14 @@ Proof.
iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver.
{ intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
- iDestruct (big_sepS_filter_acc (⊂ κ) _ _ (dom _ I) with "Halive")
+ iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
as "[Halive Halive']".
{ intros κ'. rewrite elem_of_dom. eauto. }
iApply fupd_trans. iApply fupd_mask_mono; first by apply union_subseteq_l.
iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
{ rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
iExists (dom _ B), P. rewrite !gset_to_gmap_dom -map_fmap_compose.
- rewrite (map_fmap_ext _ ((1%Qp,) ∘ to_agree) B); last naive_solver.
+ rewrite (map_fmap_ext _ ((1%Qp,.) ∘ to_agree) B); last naive_solver.
iFrame. }
rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(?&HI&Halive)".
iSpecialize ("Halive'" with "Halive").
@@ -100,7 +100,7 @@ Proof.
Qed.
Definition kill_set (I : gmap lft lft_names) (Λ : atomic_lft) : gset lft :=
- filter (Λ ∈) (dom (gset lft) I).
+ filter (Λ ∈.) (dom (gset lft) I).
Lemma elem_of_kill_set I Λ κ : κ ∈ kill_set I Λ ↔ Λ ∈ κ ∧ is_Some (I !! κ).
Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index f2acef14..19961dbf 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -74,7 +74,7 @@ Definition to_lft_stateR (b : bool) : lft_stateR :=
if b then Cinl 1%Qp else Cinr ().
Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
-Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
+Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,.) ∘ to_agree).
Section defs.
Context `{!invG Σ, !lftG Σ}.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index e3ab4f51..27368e21 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -258,8 +258,8 @@ Instance lft_inhabited : Inhabited lft := _.
Instance bor_idx_inhabited : Inhabited bor_idx := _.
Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
-Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓) := _.
-Instance lft_intersect_inj_2 κ : Inj eq eq (⊓ κ) := _.
+Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
+Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
Instance lft_intersect_right_id : RightId eq static (⊓) := _.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 28fa316e..d0b9063f 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -51,7 +51,7 @@ Section lft_contexts.
- iDestruct "H" as "[Hq Hq']".
iDestruct "Hq" as (κ0) "(% & Hq & #?)".
iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
- rewrite (inj ((lft_intersect_list κs) ⊓) κ0' κ0); last congruence.
+ rewrite (inj ((lft_intersect_list κs) ⊓.) κ0' κ0); last congruence.
iExists κ0. by iFrame "∗%".
Qed.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 3f66f559..b563e6eb 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -166,8 +166,8 @@ Section ofe.
Instance type_dist : Dist type := type_dist'.
Let T := prodO
- (prodO natO (thread_id -d> list val -d> iProp Σ))
- (lft -d> thread_id -d> loc -d> iProp Σ).
+ (prodO natO (thread_id -d> list val -d> iPropO Σ))
+ (lft -d> thread_id -d> loc -d> iPropO Σ).
Let P (x : T) : Prop :=
(∀ κ tid l, Persistent (x.2 κ tid l)) ∧
(∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1⌝) ∧
@@ -231,7 +231,7 @@ Section ofe.
st_dist' n ty1 ty2.
Instance st_dist : Dist simple_type := st_dist'.
- Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> iProp Σ :=
+ Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> iPropO Σ :=
λ tid vl, ty.(ty_own) tid vl.
Definition st_ofe_mixin : OfeMixin simple_type.
--
GitLab