From 455be6394f1cd2ffe49ad65e6f52e95cc7501e7f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Mar 2017 21:54:14 +0100
Subject: [PATCH] Update Iris.
---
opam.pins | 2 +-
theories/typing/lib/rc.v | 3 +--
2 files changed, 2 insertions(+), 3 deletions(-)
diff --git a/opam.pins b/opam.pins
index a1c04ed5..4e9b917a 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq ea7913081b7554d4d8191c0cfe99bfd736d22343
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 3d6525a57844edcc8868ec9271a0966bcc2a5e89
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 583aec81..b546de5b 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -163,8 +163,7 @@ Section code.
{ iExists None. auto. }
iSpecialize ("Hνend" with "[Hν1 Hν2]").
{ rewrite -H0. iFrame. }
- iApply wp_mask_mono; last iApply (wp_step_fupd with "Hνend"); [done..|try solve_ndisj|].
- { (* FIXME: solve_ndisj should solve this... *) set_solver+. }
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "Hνend"); [done..|solve_ndisj|].
wp_read. iIntros "#Hν". iMod ("Hν†" with "Hν") as "Hown". iModIntro.
iApply "HΦ". iFrame. iLeft. auto with iFrame.
+ destruct Hst as [[??%leibniz_equiv]|[[q'' Hqa%leibniz_equiv] ?%pos_included]%prod_included].
--
GitLab