From a4e9ac6657070c062ba437da05ee233d8b316878 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Feb 2017 21:54:10 +0100
Subject: [PATCH] Bumb Iris version.

---
 opam.pins                            | 2 +-
 theories/typing/type.v               | 5 ++---
 theories/typing/unsafe/refcell/ref.v | 6 ++----
 3 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/opam.pins b/opam.pins
index c4d725d3..7da43734 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq d1ec2aec60d1f069d5ed15282d7a2cfd1e8fb499
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 8b9f59ab3630176149621661c8f3ee7b456dfe5f
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 37f2f538..ef591793 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -461,12 +461,11 @@ Section weakening.
     E1 ⊆+ E2 → L1 ⊆+ L2 →
     subtype E1 L1 ty1 ty2 → subtype E2 L2 ty1 ty2.
   Proof.
-    (* TODO: There's no lemma relating `contains` to membership (∈)...?? *)
-    iIntros (HE12 [L' HL12]%submseteq_Permutation Hsub) "#LFT HE HL".
+    iIntros (HE12 ? Hsub) "#LFT HE HL".
     iApply (Hsub with "LFT [HE] [HL]").
     - rewrite /elctx_interp_0. by iApply big_sepL_submseteq.
     - iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
-      rewrite HL12. set_solver.
+      eauto using elem_of_submseteq.
   Qed.
 End weakening.
 
diff --git a/theories/typing/unsafe/refcell/ref.v b/theories/typing/unsafe/refcell/ref.v
index 3996978f..d3ccd14b 100644
--- a/theories/typing/unsafe/refcell/ref.v
+++ b/theories/typing/unsafe/refcell/ref.v
@@ -28,7 +28,7 @@ Section ref.
              ▷ (α ⊑ β) ∗ ▷ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
              &na{κ, tid, refcell_refN}(own γ (◯ reading_st q ν)) |}%I.
   Next Obligation.
-    iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
+    iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]"; auto.
   Qed.
   Next Obligation.
     iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
@@ -49,9 +49,7 @@ Section ref.
     iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
     iMod (bor_persistent_tok with "LFT Hinv Htok") as "[#Hinv $]". done.
     iMod (bor_sep with "LFT Hb") as "[Hκν Hb]". done.
-    (* FIXME : I cannot write #Hκν directly. *)
-    iDestruct (frac_bor_lft_incl with "LFT >[Hκν]") as "Hκν";
-      last iDestruct "Hκν" as "#Hκν".
+    iDestruct (frac_bor_lft_incl with "LFT >[Hκν]") as "#Hκν".
     { iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
     iMod (bor_na with "Hb") as "#Hb". done. eauto 20.
   Qed.
-- 
GitLab