diff --git a/opam b/opam
index b1661244092b46a44ff0148149c2b7af232b68d0..b438a948ce4de320c914917ad0d3815ff83dbf2c 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2017-11-07.2") | (= "dev") }
+  "coq-iris" { (= "dev.2017-11-11.0") | (= "dev") }
 ]
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 78f08a316c71084c4a7b4e497ee24e675c617314..488f8293680505a242d201e693dbf40dd2741b4a 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -43,7 +43,7 @@ Module Type lifetime_sig.
   Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope.
 
   Infix "⊑" := lft_incl (at level 70) : uPred_scope.
-  Infix "⊓" := lft_intersect (at level 40) : C_scope.
+  Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
 
   Section properties.
   Context `{invG, lftG Σ}.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 136adc2b37848feeff7ad20a26999ecc8a293ce9..22988966a663cc6ce7dd7740c6bfa236539e0b9d 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -20,7 +20,7 @@ End lft_notation.
 Definition static : lft := (∅ : gmultiset _).
 Definition lft_intersect (κ κ' : lft) : lft := κ ∪ κ'.
 
-Infix "⊓" := lft_intersect (at level 40) : C_scope.
+Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
 
 Inductive bor_state :=
   | Bor_in