From 8a13d68559a7443811b1614a102b53a02fd1ba44 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 16 Mar 2020 15:24:41 +0100
Subject: [PATCH] =?UTF-8?q?Bump=20Iris=20(=E2=8A=A2=20changes).?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 opam                             | 2 +-
 theories/channel/proto_channel.v | 2 +-
 theories/examples/map_reduce.v   | 2 +-
 theories/utils/compare.v         | 2 +-
 theories/utils/contribution.v    | 4 ++--
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/opam b/opam
index 1c27005..1d0d088 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris" { (= "dev.2020-03-10.6.79f576aa") | (= "dev") }
+  "coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") }
 ]
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index 013f028..2a4ab30 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -411,7 +411,7 @@ Section proto.
     iProto_le p1 p2 ≡ iProto_le_aux (fixpoint iProto_le_aux) p1 p2.
   Proof. apply: (fixpoint_unfold iProto_le_aux). Qed.
 
-  Lemma iProto_le_refl p : iProto_le p p.
+  Lemma iProto_le_refl p : ⊢ iProto_le p p.
   Proof.
     iLöb as "IH" forall (p). destruct (proto_case p) as [->|([]&pc&->)].
     - rewrite iProto_le_unfold. iLeft; by auto.
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 5b16011..7796450 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -116,7 +116,7 @@ Section mapper.
   Proof. intros [i1 y1] [i2 y2]. destruct (total (≤)%Z i1 i2); [left|right]; done. Qed.
   Instance RZB_trans : Transitive RZB.
   Proof. by apply (prod_relation_trans _). Qed.
-  Lemma RZB_cmp_spec : cmp_spec IZB RZB cmpZfst.
+  Lemma RZB_cmp_spec : ⊢ cmp_spec IZB RZB cmpZfst.
   Proof.
     iIntros ([i1 y1] [i2 y2] v1 v2) "!>"; iIntros (Φ) "[HI1 HI2] HΦ".
     iDestruct "HI1" as (w1 ->) "HI1". iDestruct "HI2" as (w2 ->) "HI2 /=".
diff --git a/theories/utils/compare.v b/theories/utils/compare.v
index 909604a..e4f7453 100644
--- a/theories/utils/compare.v
+++ b/theories/utils/compare.v
@@ -15,7 +15,7 @@ Definition cmp_spec `{!heapG Σ} {A} (I : A → val → iProp Σ)
 Definition IZ `{!heapG Σ} (x : Z) (v : val) : iProp Σ := ⌜v = #x⌝%I.
 Definition cmpZ : val := λ: "x" "y", "x" ≤ "y".
 
-Lemma cmpZ_spec `{!heapG Σ} : cmp_spec IZ (≤) cmpZ.
+Lemma cmpZ_spec `{!heapG Σ} : ⊢ cmp_spec IZ (≤) cmpZ.
 Proof.
   rewrite /IZ. iIntros (x x' v v' Φ [-> ->]) "!> HΦ".
   wp_lam. wp_pures. by iApply "HΦ".
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index bd9991a..d63da5b 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -50,7 +50,7 @@ Section contribution.
   Global Instance client_proper γ : Proper ((≡) ==> (≡)) (client γ).
   Proof. apply (ne_proper _). Qed.
 
-  Lemma contribution_init : (|==> ∃ γ, server γ 0 ε)%I.
+  Lemma contribution_init : ⊢ |==> ∃ γ, server γ 0 ε.
   Proof.
     iMod (own_alloc (● (Some (Cinr (Excl ()))) ⋅ ◯ (Some (Cinr (Excl ())))))
       as (γ) "[Hγ Hγ']"; first by apply auth_both_valid_2.
@@ -152,7 +152,7 @@ Section contribution.
 
   (** Derived *)
   Lemma contribution_init_pow n :
-    (|==> ∃ γ, server γ n ε ∗ [∗] replicate n (client γ ε))%I.
+    ⊢ |==> ∃ γ, server γ n ε ∗ [∗] replicate n (client γ ε).
   Proof.
     iMod (contribution_init) as (γ) "Hs". iExists γ.
     iInduction n as [|n] "IH"; simpl; first by iFrame.
-- 
GitLab