From 98be0049470c3ed274988b73e8c1f1dda3486f50 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Feb 2017 21:48:51 +0100
Subject: [PATCH] Bump Iris version and make use of improved solve_ndisj.

---
 opam.pins                               | 2 +-
 theories/typing/own.v                   | 6 ++----
 theories/typing/uniq_bor.v              | 1 -
 theories/typing/unsafe/cell.v           | 3 +--
 theories/typing/unsafe/refcell/refmut.v | 1 -
 5 files changed, 4 insertions(+), 9 deletions(-)

diff --git a/opam.pins b/opam.pins
index aa62552e..215997ac 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7b36d0e4c312b99b081f05b6575071b56bf12a55
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 857f9909b773754d521d47f0fe6f43aec6c3214d
diff --git a/theories/typing/own.v b/theories/typing/own.v
index e1786c94..b3707114 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -77,12 +77,10 @@ Section own.
           with "[Hpbown]") as "#Hinv"; first by eauto.
     iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_later with "LFT [Hbtok]") as "Hb".
-      { apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
+    - iMod (bor_later with "LFT [Hbtok]") as "Hb"; first solve_ndisj.
       { rewrite bor_unfold_idx. eauto. }
       iModIntro. iNext. iMod "Hb".
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]".
-      { apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
+      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; first solve_ndisj.
       iApply "Hclose". auto.
     - iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
       iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 88055127..e5792895 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -7,7 +7,6 @@ Set Default Proof Using "Type".
 
 Section uniq_bor.
   Context `{typeG Σ}.
-  Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
 
   Program Definition uniq_bor (κ:lft) (ty:type) :=
     {| ty_size := 1;
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index f3009fae..554c95ef 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -8,7 +8,6 @@ Set Default Proof Using "Type".
 
 Section cell.
   Context `{typeG Σ}.
-  Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
 
   Program Definition cell (ty : type) :=
     {| ty_size := ty.(ty_size);
@@ -50,7 +49,7 @@ Section cell.
     intros ty Hcopy. split; first by intros; simpl; apply _.
     iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
     (* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
-    destruct (ty_size ty) as [|sz] eqn:Hsz.
+    destruct (ty_size ty) as [|sz] eqn:Hsz; simpl in *.
     { iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
       iDestruct "Hown" as (vl) "[H↦ #Hown]".
       simpl. assert (F ∖ ∅ = F) as -> by set_solver+.
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/unsafe/refcell/refmut.v
index 3817d1ad..1c7b2b00 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/unsafe/refcell/refmut.v
@@ -8,7 +8,6 @@ Set Default Proof Using "Type".
 
 Section refmut.
   Context `{typeG Σ, refcellG Σ}.
-  Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
 
   Program Definition refmut (α : lft) (ty : type) :=
     {| ty_size := 2;
-- 
GitLab