From ebddbb7fa7c0a6891be35c04a570f837c7bd2c0c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 May 2017 10:49:11 +0200
Subject: [PATCH] Bump Iris.

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

diff --git a/opam.pins b/opam.pins
index 982bbc18..614a4d53 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7127e55309477c4a1db2cd43d58f65efa3431171
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 646bfc85e7ea6313e62feecf4ebcbcd76a186e71
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 29f20d78..403ddcff 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -274,7 +274,7 @@ Section typing.
       { iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
       iApply ("Hf" with "LFT [] Htl [Htk] [Hk HÎºsI HL]").
       + iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
-        iInduction Îºs as [|Îº Îºs] "IH" forall "HÎºs"=> //=. iSplitL.
+        iInduction Îºs as [|Îº Îºs] "IH"=> //=. iSplitL.
         { iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
         iApply "IH". iAlways. iApply lft_incl_trans; first done. iApply lft_intersect_incl_r.
       + iSplitL; last done. iExists Ï. iSplit; first by rewrite /= left_id.
-- 
GitLab