From a0c78ebcb5dbbea150942332fa45adac0a43a74e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 May 2020 11:14:28 +0200
Subject: [PATCH] Bump Iris (sbi removal).

---
 opam                                  | 4 ++--
 theories/lifetime/frac_borrow.v       | 2 +-
 theories/lifetime/lifetime_sig.v      | 2 +-
 theories/lifetime/model/boxes.v       | 4 ++--
 theories/lifetime/model/definitions.v | 4 ++--
 theories/typing/lib/rwlock/rwlock.v   | 2 +-
 6 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/opam b/opam
index 340f66ec..ee674c09 100644
--- a/opam
+++ b/opam
@@ -9,14 +9,14 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git"
 
 synopsis: "LambdaRust Coq formalization (weak memory branch)"
 description: """
-A formal model of a Rust core langauge and type system, a logical relation for
+A formal model of a Rust core language and type system, a logical relation for
 the type system, and safety proof for some Rust libraries.
 
 This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-05-08.0.29d1f725") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-05-24.0.d58f8824") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 5dcefa91..e4c6fb34 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -126,7 +126,7 @@ Section frac_bor.
     destruct (Qp_lower_bound (qκ'/2) (qφ0/2)) as (qq & qκ'0 & qφ0' & Hqκ' & Hqφ).
     iExists qq.
     iAssert (▷ φ qq ∗ ⎡▷ φ' (qφ0' + qφ0 / 2) V0⎤)%Qp%I with "[Hφ0]" as "[$ Hqφ]".
-    { rewrite -{1}(Qp_div_2 qφ0) {1}Hqφ -assoc_L embed_later -bi.later_sep. iNext.
+    { rewrite -{1}(Qp_div_2 qφ0) {1}Hqφ -assoc_L !embed_later -bi.later_sep. iNext.
       iDestruct ("Hfrac" with "Hφ0") as "[Hφ0 $]". iApply "Hφ'".
       by iApply (monPred_in_elim with "HV0"). }
     iAssert (▷ ⎡own γ qq⎤ ∗
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 859c948c..9c3fca84 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -28,7 +28,7 @@ Module Type lifetime_sig.
 
   Section defs.
   Context {Σ : gFunctors} {Lat}.
-  Notation monPred := (monPredSI (lat_bi_index Lat) (uPredSI (iResUR Σ))).
+  Notation monPred := (monPredI (lat_bi_index Lat) (uPredI (iResUR Σ))).
 
   Parameter lft_ctx : ∀ `{!invG Σ, !lftG Lat E0 Σ}, iProp Σ.
 
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 3e04130f..7d42ddc2 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -24,7 +24,7 @@ Proof. solve_inG. Qed.
 Section box_defs.
   Context `{invG Σ, boxG Lat Σ} (N : namespace).
   Notation iProp := (iProp Σ).
-  Notation monPred := (monPred (lat_bi_index Lat) (uPredSI (iResUR Σ))).
+  Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
 
   Definition slice_name := gname.
 
@@ -56,7 +56,7 @@ Instance: Params (@box) 6 := {}.
 Section box.
 Context `{invG Σ, boxG Lat Σ} (N : namespace).
 
-Notation monPred := (monPred (lat_bi_index Lat) (uPredSI (iResUR Σ))).
+Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
 Implicit Types P Q : monPred.
 
 Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 9841715d..53db3b02 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -87,7 +87,7 @@ Section defs.
   Context {Σ Lat} `{!invG Σ, !lftG Lat E0 Σ}.
 
   Notation iProp := (iProp Σ).
-  Notation monPred := (monPredSI (lat_bi_index Lat) (uPredSI (iResUR Σ))).
+  Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
 
   Definition lft_tok (q : Qp) (κ : lft) : monPred :=
     ([∗ mset] Λ ∈ κ, ∃ V, monPred_in V ∗
@@ -241,7 +241,7 @@ Context `{!invG Σ, !lftG Lat E0 Σ}.
 Implicit Types κ : lft.
 
 Notation iProp := (iProp Σ).
-Notation monPred := (monPred (lat_bi_index Lat) (uPredSI (iResUR Σ))).
+Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
 
 (* Unfolding lemmas *)
 Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → monPred) Vs I n :
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 1af88df8..5efbe556 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -216,7 +216,7 @@ Section rwlock_inv.
   Proof.
     move => ???.
     apply bi.sep_ne; [|apply bi.sep_ne]; [..|done];
-      apply bi.later_contractive; (destruct n; [done|]);
+      f_contractive;
       apply bi.intuitionistically_ne.
     - apply bi.iff_ne; [done|]. apply bi.exist_ne => ?.
       apply bi.sep_ne; [done|by apply ty_own_type_dist].
-- 
GitLab