From 8fbabc925b1544e8f99c9d85f068bb58b9410bb9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 26 Jan 2017 22:58:59 +0100
Subject: [PATCH] Fix compilation with latest Iris.
---
opam.pins | 2 +-
theories/typing/type_sum.v | 2 +-
theories/typing/unsafe/refcell/ref_code.v | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/opam.pins b/opam.pins
index ccdcb41f..e603372b 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 939b747baa303ca3e2e1538cfd76fccd900596cf
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2550dff5c235a7367390a26c0db9871adb8fe0e7
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 3df1f459..a529af73 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -233,7 +233,7 @@ Section case.
rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
iDestruct (ty_size_eq with "Hty") as "#>%".
- iApply wp_fupd. iApply (wp_memcpy with "[$H↦vl1 $H↦2]"); [|lia|].
+ iApply (wp_memcpy with "[$H↦vl1 $H↦2]"); [|lia|].
{ rewrite take_length. lia. }
iNext; iIntros "[H↦vl1 H↦2]".
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index 97284a3b..a8706659 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -52,7 +52,7 @@ Section ref_functions.
revert Heq. intros [= <-]. destruct st'' as [[ag q'] n].
revert Hle=>/Some_included_2 /Some_pair_included
[/Some_pair_included_total_1 [/agree_included Heq _] _] [[Hag _] _].
- iExists q', n. iPureIntro. repeat constructor. apply Cinlr_equiv.
+ iExists q', n. iPureIntro. repeat constructor. apply Cinr_equiv.
do 2 constructor; last done. apply agree_op_inv. by rewrite comm -Heq. }
iDestruct "Hst" as %[st' [-> Hst']]%equiv_Some_inv_r'.
destruct st' as [|[[]]|]; try by inversion Hst'. apply (inj Cinr), (inj2 pair) in Hst'.
--
GitLab