From 7b72dbb807eac7cb55d9cc3014caf26f0b1d4bb9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 10 Mar 2017 00:04:56 +0100
Subject: [PATCH] Bump Iris and fix some minor things.
---
opam.pins | 2 +-
theories/typing/lib/rc.v | 2 +-
theories/typing/sum.v | 9 ++++-----
3 files changed, 6 insertions(+), 7 deletions(-)
diff --git a/opam.pins b/opam.pins
index ad8c09a8..20266490 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq a1bf05fe892801c43a9d61e8cb7cf7cb1f1eced3
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1e241cca15302ae89d41f14251c2dafbd7efebb6
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index b0cb325a..976381bb 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -88,7 +88,7 @@ Section rc.
iExists _, _, _. iFrame. done. }
iDestruct "HX" as (γ ν q') "(#Hinv & Hrc & Htok & #Hshr)".
iMod ("Hclose2" with "[] [Hrc Htok]") as "[HX Htok]".
- { iNext. iIntros "HX". iModIntro. (* FIXME: iNext here doesn't strip of the next from in front of the evar. *)
+ { iNext. iIntros "HX". iModIntro. iNext.
iRight. iExists γ, ν, q'. iExact "HX". }
{ iNext. by iFrame "#∗". }
iAssert (|={F ∖ ↑shrN}=> C)%I with "[HX]" as ">#HC".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 3fadde0b..5ef44d37 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -205,11 +205,10 @@ Section sum.
{ rewrite <-HF. simpl. rewrite <-union_subseteq_r.
apply shr_locsE_subseteq. omega. }
iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
- { (* Really, we don't even have a lemma for anti-monotonicity of difference...? *)
- cut (shr_locsE (shift_loc l 1) (ty_size (nth i tyl ∅)) ⊆
- shr_locsE (shift_loc l 1) (list_max (map ty_size tyl))).
- - simpl. set_solver+.
- - apply shr_locsE_subseteq. omega. }
+ { apply difference_mono_l.
+ trans (shr_locsE (shift_loc l 1) (list_max (map ty_size tyl))).
+ - apply shr_locsE_subseteq. omega.
+ - set_solver+. }
destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
rewrite -(heap_mapsto_pred_op _ q' q'02); last (by intros; apply ty_size_eq).
rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).
--
GitLab