From 0beac34686103d71d6fd6604e78ffb8753c45ad1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 5 Oct 2020 19:09:17 +0200
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/lifetime/model/boxes.v | 12 ++++++------
theories/lifetime/model/reborrow.v | 2 +-
3 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/opam b/opam
index 61d0d843..d1175a57 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-10-01.0.7fcd4a3d") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-10-05.0.0974bf5a") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 4a3ac825..aaffe540 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -12,7 +12,7 @@ Implicit Types Lat : latticeT.
Class boxG Lat Σ :=
boxG_inG :> inG Σ (prodR
(authR (optionUR (exclR (optionO (latO Lat)))))
- (optionR (agreeR (laterO (Lat -d> iPrePropO Σ))))).
+ (optionR (agreeR (laterO (Lat -d> iPropO Σ))))).
Definition boxΣ Lat : gFunctors := #[
GFunctor (authR (optionUR (exclR (optionO (latO Lat)))) *
@@ -32,7 +32,7 @@ Section box_defs.
own γ (a, ε).
Definition box_own_prop (γ : slice_name) (P : monPred) : iProp :=
- own γ (ε, Some (to_agree (Next (iProp_unfold ∘ P : _ -d> _)))).
+ own γ (ε, Some (to_agree (Next (P : _ -d> _)))).
Definition slice_inv (γ : slice_name) (P : monPred) : iProp :=
(∃ o, box_own_auth γ (● Excl' o) ∗ from_option (P ∘ of_latT) True o)%I.
@@ -60,11 +60,11 @@ Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
Implicit Types P Q : monPred.
Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
-Proof. unfold box_own_prop. intros ????. (do 5 f_equiv)=>? /=. by do 2 f_equiv. Qed.
+Proof. unfold box_own_prop. intros ????. (do 5 f_equiv)=>? /=. by f_equiv. Qed.
Global Instance box_own_prop_contractive γ : Contractive (box_own_prop γ).
Proof.
unfold box_own_prop. intros ????.
- do 4 f_equiv. f_contractive=>? /=. by do 2 f_equiv.
+ do 4 f_equiv. f_contractive=>? /=. by f_equiv.
Qed.
Global Instance box_own_auth_proper γ : Proper ((≡) ==> (≡)) (box_own_auth γ).
@@ -111,7 +111,7 @@ Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
iIntros "#HQ". iApply monPred_equivI. iIntros (V).
- iApply iProp_unfold_equivI. rewrite discrete_fun_equivI. iNext. iApply "HQ".
+ rewrite discrete_fun_equivI. iNext. iApply "HQ".
Qed.
Lemma box_alloc : ⊢ box N ∅ True.
@@ -125,7 +125,7 @@ Lemma slice_insert_empty E q f Q P :
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iMod (own_alloc_cofinite (● Excl' None ⋅ ◯ Excl' None,
- Some (to_agree (Next ((λ V, iProp_unfold (Q V)) : _ -d> _)))) (dom _ f))
+ Some (to_agree (Next (Q : _ -d> _)))) (dom _ f))
as (γ) "[Hdom Hγ]". { split; [by apply auth_both_valid_discrete|done]. }
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 15ce9b6f..503112e9 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -15,7 +15,7 @@ Qed.
Lemma and_extract_own `{inG Σ A} γ (x : A) (P : iProp Σ) :
own γ x ∧ P -∗ own γ x ∗ (own γ x -∗ P).
-Proof. rewrite own_eq. apply and_extract_ownM. Qed.
+Proof. rewrite own.own_eq. apply and_extract_ownM. Qed.
Lemma and_extract_own_bor `{lftG Lat E0 Σ} κ σ (P : iProp Σ) :
own_bor κ σ ∧ P -∗ own_bor κ σ ∗ (own_bor κ σ -∗ P).
--
GitLab