From 230c33db0bf988d3799ef3beca303d5b80dd377e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 22 Jun 2018 09:35:24 +0200
Subject: [PATCH] bump Iris; fix for std++ namespace lemma changes
---
opam | 2 +-
theories/examples/hashtable.v | 17 ++++-------------
2 files changed, 5 insertions(+), 14 deletions(-)
diff --git a/opam b/opam
index d1122910..d0e59d8f 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
depends: [
- "coq-iris" { (= "branch.gen_proofmode.2018-06-21.2.8ca8b776") | (= "dev") }
+ "coq-iris" { (= "branch.gen_proofmode.2018-06-21.4.f9fc75c6") | (= "dev") }
]
diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index 3f3137b6..a1dbf11c 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -1865,8 +1865,7 @@ Section proof.
wp_bind (add_item _ _)%E.
(* We need the full postcondition of add_item in the atomic shift, so we can't use LA_Inv. *)
iApply (LA_Mono _ _ _ _ _ (⊤ ∖ ↑N) with "[Hentries]");
- [| by iApply (add_item_spec with "[$]"); first omega |].
- { by apply namespaces.ndisj_subseteq_difference. }
+ [| by iApply (add_item_spec with "[$]"); first omega |]; first solve_ndisj.
unfold atomic_shift.
iExists _; iSplit; first by iCombine "Hhist Ht" as "H"; iApply "H".
iIntros "!# [>Hhist Ht]".
@@ -1967,10 +1966,7 @@ Section proof.
destruct ls as [|b3]; [discriminate|].
destruct ls; [|discriminate].
iExists b1, b2, b3, h; simpl in *; iFrame; auto. }
- iApply (fupd_mask_mono (↑escrowN)).
- { apply namespaces.ndisj_subseteq_difference; last done.
- do 2 apply namespaces.ndot_preserve_disjoint_r.
- apply namespaces.ndot_ne_disjoint; done. }
+ iApply (fupd_mask_mono (↑escrowN)); first solve_ndisj.
iMod "HX" as "#HX"; iModIntro.
unfold onceP; iFrame "#"; auto. }
iNext; iIntros "[? _]".
@@ -2172,10 +2168,7 @@ Section proof.
iPoseProof (escrow_apply with "[] [$H $Htok]") as "H".
{ iIntros "[H1 H2]".
iPoseProof (own_valid_2 with "H1 H2") as "%"; done. }
- iPoseProof (fupd_mask_mono (↑escrowN) with "H") as ">H".
- { apply namespaces.ndisj_subseteq_difference; last done.
- do 2 apply namespaces.ndot_preserve_disjoint_r.
- apply namespaces.ndot_ne_disjoint; done. }
+ iPoseProof (fupd_mask_mono (↑escrowN) with "H") as ">H"; first solve_ndisj.
iMod "H"; iModIntro; auto.
* iNext; do 2 (rewrite monPred_objectively_forall; iIntros (?)).
iApply objectively_entails.
@@ -2218,9 +2211,7 @@ Section proof.
iDestruct "H" as (lr) "(% & Hhists & Htotal)".
wp_seq.
iMod (inv_open with "Hinv") as "[Href Hclose]"; first auto.
- iApply (na_read with "[$Hctx $Htotal]"); first auto.
- { apply namespaces.ndisj_subseteq_difference; last auto.
- apply namespaces.ndot_ne_disjoint; done. }
+ iApply (na_read with "[$Hctx $Htotal]"); first auto; first solve_ndisj.
iNext; iIntros (?) "[% Htotal]"; subst.
iDestruct (monPred_objectively_elim with "Href") as (HT) "[HH Href]".
iDestruct "Href" as (hr) "[% Href]".
--
GitLab