From b6993ddcce42013d2f95f18f5967b0ceae4f4f9a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Nov 2017 11:05:29 +0100
Subject: [PATCH] Bump Iris.

---
 opam                                  | 2 +-
 theories/lifetime/lifetime_sig.v      | 2 +-
 theories/lifetime/model/definitions.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/opam b/opam
index b1661244..b438a948 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 78f08a31..488f8293 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 136adc2b..22988966 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
-- 
GitLab