diff --git a/opam b/opam
index 4b1891b800a4e3f21205dd4687bf5415a11ca102..8da289fd4cb64e49470ad7a6beb5efafeecc6f6a 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2019-12-13.0.335ff6d7") | (= "dev") }
+  "coq-iris" { (= "dev.2020-01-17.1.5088d5b0") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 19961dbf34a6f26f3037e38e22f240856ff683dc..05cb652b8cf40335d605fa862826b590a22c9098 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -230,7 +230,7 @@ Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) I n :
   (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
   lft_vs_inv_go κ f I ≡{n}≡ lft_vs_inv_go κ f' I.
 Proof.
-  intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ'.
+  intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ' _.
   by apply forall_ne=> Hκ.
 Qed.