From 5ab668f369761fce65dffb7f18ec931b5178189c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 23 Jul 2021 11:58:08 +0200
Subject: [PATCH] bump Iris; use solve_ndisj more

---
 coq-lambda-rust.opam                              | 2 +-
 theories/typing/lib/rwlock/rwlockreadguard_code.v | 6 +-----
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 7ab5190e..c8e90773 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-07-22.0.26ebf1ee") | (= "dev") }
+  "coq-iris" { (= "dev.2021-07-23.2.572da574") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index fadb5089..4cd8f7ca 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -95,11 +95,7 @@ Section rwlockreadguard_functions.
           rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv.
           iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
           iApply (step_fupd_mask_mono ((↑lftN ∪ lft_userE) ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ lft_userE)));
-            last iApply (step_fupd_mask_frame_r _ (lft_userE)).
-          { solve_ndisj. }
-          { solve_ndisj. }
-          { rewrite difference_difference. apply: disjoint_difference_r1. done. }
-          { solve_ndisj. }
+            last iApply (step_fupd_mask_frame_r _ (lft_userE)); [solve_ndisj..|].
           iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
           iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hh" with "H†") as "Hb".
           { set_solver+. }
-- 
GitLab