From 0d9e2d1bb8d884100f2a44c90709821e0da3bba0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 5 Jun 2019 09:30:58 +0200
Subject: [PATCH] Bump Iris.

---
 opam                                            | 2 +-
 theories/barrier/example_joining_existentials.v | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/opam b/opam
index 89cd8efa..a1dcd1b9 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.2019-06-03.2.b368c861") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-04.2.322cdf37") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/barrier/example_joining_existentials.v b/theories/barrier/example_joining_existentials.v
index c30d462a..40cd79b3 100644
--- a/theories/barrier/example_joining_existentials.v
+++ b/theories/barrier/example_joining_existentials.v
@@ -7,9 +7,9 @@ From iris_examples.barrier Require Import proof specification.
 Set Default Proof Using "Type".
 
 Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
-  csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
+  csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ) _).
 Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()).
-Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ)) : one_shotR Σ F :=
+Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ) _) : one_shotR Σ F :=
   Cinr $ to_agree $ Next $ cFunctor_map F (iProp_fold, iProp_unfold) x.
 
 Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
@@ -28,7 +28,7 @@ Section proof.
 Local Set Default Proof Using "Type*".
 Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
 Context (N : namespace).
-Local Notation X := (F (iProp Σ)).
+Local Notation X := (F (iProp Σ) _).
 
 Definition barrier_res γ (Φ : X → iProp Σ) : iProp Σ :=
   (∃ x, own γ (Shot x) ∗ Φ x)%I.
-- 
GitLab