diff --git a/opam b/opam
index 1c2700563efabb5b88deefbedf2676b3e0b477b4..1d0d0888047db292977babf3978c9f794e7df87d 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 013f028c7d1f431ee0a9e8704097be555bea263b..2a4ab30198764fd96e287c83c43b2ba542296d03 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 5b1601123408f53df4a712ee2ec5492f8c12f88d..77964506070a112a902ff84c0e7d8aac2c5b3484 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 909604a96c6c8142535d07bb274acf3bb5300066..e4f7453d964939a7b50367284f67aadadece1f3d 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 bd9991ae06eba627ea03c15060f2067aea0fc28a..d63da5b2e238f79b4650af952cc7519129b7321e 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.