From b91fe2270ec3ea7568fd2c6378c8514505590ad9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Mar 2017 16:57:00 +0100
Subject: [PATCH] update to latest Iris
---
opam.pins | 2 +-
theories/typing/lft_contexts.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam.pins b/opam.pins
index 629a8a4a..a96d0bbb 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 039f9fd5f753337034dcbfbbdb311cebdfa93acf
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq c798ff4f78cd663c2a710b0af4e7af063b35580a
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index de2276bc..c4f15b94 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -342,7 +342,7 @@ Section lft_contexts.
iMod (HE1 with "HE1 HL1") as (qE1) "[HE1 Hclose1]". done.
iMod (HE2 with "HE2 HL2") as (qE2) "[HE2 Hclose2]". done.
destruct (Qp_lower_bound qE1 qE2) as (q & qE1' & qE2' & -> & ->). iExists q.
- rewrite !fractional (fractional_half_equiv qE) /elctx_interp big_sepL_app.
+ rewrite !fractional [elctx_interp E qE]fractional_half /elctx_interp big_sepL_app.
iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]". iIntros "!> [Hq1 Hq2]".
iMod ("Hclose1" with "[$HE1 $Hq1]") as "[$ $]". iApply "Hclose2". iFrame.
Qed.
--
GitLab