From 5592afd444665dcd89336587a6b73cb0cc9b7e74 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Mar 2017 15:20:43 +0200
Subject: [PATCH] Bump Iris and fix some stuff.

---
 opam.pins                | 2 +-
 theories/typing/lib/rc.v | 5 +----
 theories/typing/sum.v    | 1 -
 3 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/opam.pins b/opam.pins
index 83c77af5..9d0b4a49 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7dec931b3ce0674c093a325275976aac96e9c8e6
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0429c257e3088cf77c8852a2cbeff2b02671b8b5
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index b05eb1fc..4f67aa13 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -154,10 +154,7 @@ Section rc.
   Lemma rc_subtype ty1 ty2 :
     type_incl ty1 ty2 -∗ type_incl (rc ty1) (rc ty2).
   Proof.
-    iIntros "#Hincl". iPoseProof "Hincl" as "Hincl2".
-    iDestruct "Hincl2" as "(#Hsz & #Hoincl & #Hsincl)".
-    (* FIXME: Would be nice to have an easier way to duplicate
-       destructed things.  Maybe iPoseProof with a destruct pattern? *)
+    iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
     iSplit; first done. iSplit; iAlways.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl & H† & Hc) | Hvl]".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index d3b4a77c..1b88e917 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -141,7 +141,6 @@ Section sum.
     { iInduction Htyl as [|???? Hsub] "IH".
       { iClear "∗". iIntros "!# _". done. }
       iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
-      (* FIXME: WHy does the previous iDestruvt remove HL? *)
       iAlways. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
       iDestruct ("IH" with "HE") as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
     iDestruct (subtype_Forall2_llctx with "HL") as "#Htyl"; first done.
-- 
GitLab