diff --git a/opam b/opam
index 68f1fb3f8ed2eaee91bb5c3adddf332b5e767916..b0c9568551efe4a1c8468e34e78e4f09d269e279 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-05-28.3.38f177d3") | (= "dev") }
+  "coq-iris" { (= "dev.2020-06-18.3.5f98a0bf") | (= "dev") }
 ]
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index d63da5b2e238f79b4650af952cc7519129b7321e..eae3ada9f672329e392a32d61d67b8bab36def79 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -17,7 +17,7 @@ To model this ghost theory construction, we use the camera
 [auth (option (csum (positive * A) (excl unit)))]. *)
 From iris.base_logic Require Export base_logic lib.iprop lib.own.
 From iris.proofmode Require Export tactics.
-From iris.algebra Require Import excl auth csum gmultiset.
+From iris.algebra Require Import excl auth csum gmultiset numbers.
 From iris.algebra Require Export local_updates.
 
 Class contributionG Σ (A : ucmraT) `{!CmraDiscrete A} := {