From f8f14ccf07213c77e76c7094595d4bbbd3e35563 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 7 Apr 2017 21:10:36 +0200
Subject: [PATCH] Bump Iris, fix some stuff.
---
opam.pins | 2 +-
theories/lang/lib/lock.v | 8 ++------
theories/lifetime/lifetime.v | 3 ++-
3 files changed, 5 insertions(+), 8 deletions(-)
diff --git a/opam.pins b/opam.pins
index 9d0b4a49..15d94cd4 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0429c257e3088cf77c8852a2cbeff2b02671b8b5
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq f987ca782d1301d319cf6c4ba8e2ab449ebe903a
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index fa9f7b86..680293b6 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -61,12 +61,8 @@ Section proof.
wp_seq. wp_alloc l vl as "Hl" "H†". inv_vec vl=>x.
rewrite heap_mapsto_vec_singleton. (* FIXME shouldn't this also compute now, like bigops do? *)
wp_let. wp_write.
- iMod (newlock_inplace with "[HR] Hl") as (γ) "?".
- { (* FIXME: Can we make it so that we can just say "HR" instead of "[HR]", and the
- later does not matter? Or at least, "$HR" should work. Why can't we frame
- below later? *)
- done. }
- iApply "HΦ". done.
+ iMod (newlock_inplace with "HR Hl") as (γ) "?".
+ by iApply "HΦ".
Qed.
Lemma try_acquire_spec γ l R :
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index f1e0c77e..62d715c1 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -51,7 +51,8 @@ Lemma bor_or E κ P Q :
lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
Proof.
iIntros (?) "#LFT H". rewrite uPred.or_alt.
- iMod (bor_exists with "LFT H") as ([]) "H"; auto.
+ (* The (A:=...) is needed due to Coq bug #5458 *)
+ iMod (bor_exists (A:=bool) with "LFT H") as ([]) "H"; auto.
Qed.
Lemma bor_later E κ P :
--
GitLab