From 25c37eb0063c6fba5b15987056261cb1b8ccd7c7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 22 Feb 2017 13:03:43 +0100
Subject: [PATCH] Bump Iris.

---
 opam.pins             | 2 +-
 theories/typing/own.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam.pins b/opam.pins
index bd50b2ef..b496f750 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 09d97eae9eba95ebf5539a0b32e88bfc0b61c0fe
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 02bc52b4d905eb635940ff8545d59676ad44ea8c
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 95f6ade8..8af5f19f 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -229,7 +229,7 @@ Section typing.
   Proof.
     iIntros (<- tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
-    iDestruct "Hown" as "[H↦∗: >H†]". iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
+    iDestruct "Hown" as "[H↦: >H†]". iDestruct "H↦:" as (vl) "[>H↦ Hown]".
     rewrite tctx_interp_nil. iDestruct (ty_size_eq with "Hown") as "#>EQ".
     iDestruct "EQ" as %<-. iApply (wp_delete with "[-]"); auto; [].
     rewrite freeable_sz_full. by iFrame.
-- 
GitLab