From d4c7170cd1fdac62fc4b61d6ec699479c0107b32 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 20 May 2018 11:05:40 +0200
Subject: [PATCH] bump iris; small rename fix needed

---
 opam                                         | 2 +-
 theories/lecture_notes/ccounter.v            | 4 ++--
 theories/lecture_notes/coq_intro_example_2.v | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/opam b/opam
index 1833f5b..1ed5c33 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2018-04-27.2.1ab890fc") | (= "dev") }
+  "coq-iris" { (= "dev.2018-05-17.0.463474fb") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/lecture_notes/ccounter.v b/theories/lecture_notes/ccounter.v
index 0bb2750..78b4d41 100644
--- a/theories/lecture_notes/ccounter.v
+++ b/theories/lecture_notes/ccounter.v
@@ -43,7 +43,7 @@ Section ccounter.
   Lemma is_ccounter_op γ₁ γ₂ ℓ q1 q2 (n1 n2 : nat) :
     is_ccounter γ₁ γ₂ ℓ (q1 + q2) (n1 + n2)%nat ⊣⊢ is_ccounter γ₁ γ₂ ℓ q1 n1 ∗ is_ccounter γ₁ γ₂ ℓ q2 n2.
   Proof.
-    apply uPred.equiv_spec; split; rewrite /is_ccounter frag_auth_op own_op.
+    apply uPred.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
     - iIntros "[? #?]".
       iFrame "#"; iFrame.
     - iIntros "[[? #?] [? _]]".
@@ -128,4 +128,4 @@ Section ccounter.
       simplify_eq. iApply "HΦ".
       iFrame; iFrame "#".
   Qed.
-End ccounter.
\ No newline at end of file
+End ccounter.
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index 7522450..ac1a624 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -593,7 +593,7 @@ Section ccounter.
   Lemma is_ccounter_op γ ℓ q1 q2 (n1 n2 : nat) :
     is_ccounter γ ℓ (q1 + q2) (n1 + n2)%nat ⊣⊢ is_ccounter γ ℓ q1 n1 ∗ is_ccounter γ ℓ q2 n2.
   Proof.
-    apply uPred.equiv_spec; split; rewrite /is_ccounter frag_auth_op own_op.
+    apply uPred.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
     - iIntros "[? #?]".
       iFrame "#"; iFrame.
     - iIntros "[[? #?] [? _]]".
@@ -655,4 +655,4 @@ Section ccounter.
     iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists n; by iFrame|].
     iApply "HΦ"; iModIntro. iFrame "Hown #"; done.
   Qed.
-End ccounter.
\ No newline at end of file
+End ccounter.
-- 
GitLab