diff --git a/opam b/opam
index 4f214a0e708c727e5378a40bf3a67334c5b4e2d6..f67977e4e320f240f558334f539ff6cfac27b971 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-09-15.3.986a8883") | (= "dev") }
+  "coq-iris" { (= "dev.2020-09-30.0.fe735a96") | (= "dev") }
 ]
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index eae3ada9f672329e392a32d61d67b8bab36def79..4615bd9d686e3a60b35e5ea71fbf619ea2d4277b 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -64,7 +64,7 @@ Section contribution.
   Proof.
     rewrite /server /client. case_decide=> //. iIntros "Hs Hc".
     iDestruct (own_valid_2 with "Hs Hc")
-      as %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid; first done.
+      as %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete; first done.
     move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[? _].
     by destruct (Pos.lt_irrefl 1).
   Qed.
@@ -89,7 +89,7 @@ Section contribution.
     - iDestruct "Hs" as "(_ & _ & Hc')".
       by iDestruct (own_valid_2 with "Hc Hc'") as %?.
     - iDestruct (own_valid_2 with "Hs Hc")
-        as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid.
+        as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete.
       { setoid_subst. by destruct n. }
       move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[??].
       by destruct n.