From 22f5cdcd6900d9c95d10e17e64bbd504f9cb2a35 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 22 Feb 2017 16:51:58 +0100
Subject: [PATCH] bump Iris

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

diff --git a/opam.pins b/opam.pins
index b496f750..eac97896 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 02bc52b4d905eb635940ff8545d59676ad44ea8c
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 15be3526bf8e9cff9a8cf7b97973367e0f697b6e
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 9731f5be..2ac03c24 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -33,8 +33,7 @@ Section fn.
     intros tid vl. destruct n' as [|n']; simpl; [done|]. unfold typed_body.
     do 12 f_equiv. f_contractive. do 17 f_equiv.
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
-      rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat f_equiv. apply Hty.
-      by rewrite (ty_size_ne _ _ _ (Hty _)).
+      rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat (apply Hty || f_equiv).
     - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
       cut (∀ n tid p i, Proper (dist (S n) ==> dist n)
         (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).
-- 
GitLab