diff --git a/opam.pins b/opam.pins
index aa62552e97b44b8621effdf01c0d00c9949e4b90..215997ace9c938cc08c4d4ad42a14f0959404ea2 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 e1786c942942bc08b5b6cb192e2edcd6994ec8e5..b3707114cc5a1550482ec178eee88b82204aa590 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 88055127b5897ca6a70289dd531a765ec2382ab9..e5792895343245cd7e94533e53a9d6dc4f83e8e3 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 f3009fae66883bb4d4f1edf40e8e3641322e7246..554c95ef47b1bc862085f670ba129c7ad851fba1 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 3817d1ad94d94ded1606435b6e534baf1b00bc0f..1c7b2b00fe2bc8622c70e145f4cba9dbd70967c0 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;