From 029249474799ad20e4a78e80ee918f52a6800e40 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Mar 2017 01:14:58 +0200
Subject: [PATCH] Avoid set_solver in favor of solve_ndisj.

---
 opam.pins                                     |  2 +-
 theories/lifetime/model/accessors.v           |  2 +-
 theories/typing/borrow.v                      | 14 +++++------
 theories/typing/function.v                    |  2 +-
 theories/typing/lib/rc.v                      |  2 +-
 theories/typing/lib/refcell/refmut.v          |  4 ++--
 theories/typing/lib/rwlock/rwlockwriteguard.v |  4 ++--
 theories/typing/own.v                         | 16 ++++++-------
 theories/typing/product.v                     | 12 +++++-----
 theories/typing/product_split.v               |  6 ++---
 theories/typing/shr_bor.v                     |  7 +++---
 theories/typing/sum.v                         | 10 ++++----
 theories/typing/type.v                        | 10 ++++----
 theories/typing/uniq_bor.v                    | 24 +++++++++----------
 theories/typing/util.v                        | 12 +++++-----
 15 files changed, 63 insertions(+), 64 deletions(-)

diff --git a/opam.pins b/opam.pins
index 3581188d..83c77af5 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq e906ef70877d20c63a36f791a9d6620b613695a8
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7dec931b3ce0674c093a325275976aac96e9c8e6
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index da53e273..7362f5e8 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -62,7 +62,7 @@ Proof.
   iIntros "#HEQ Hvs HvsQ". iNext. rewrite !lft_vs_unfold.
   iDestruct "Hvs" as (n) "[Hcnt Hvs]". iExists n.
   iIntros "{$Hcnt}*Hinv[HQ HPb] #H†". iApply fupd_trans.
-  iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP". set_solver.
+  iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP"; first solve_ndisj.
   iModIntro. iAssert (â–· Pb)%I with "[HPb HP]" as "HPb".
   { iNext. iRewrite "HEQ". iFrame. }
   iApply ("Hvs" with "Hinv HPb H†").
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index d3f7b676..bc24f8fa 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -48,7 +48,7 @@ Section borrow.
   Proof.
     iIntros (Hκ tid) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
-    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
+    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
@@ -78,12 +78,12 @@ Section borrow.
   Proof.
     iIntros (Hκ tid) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
-    iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
+    iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iDestruct "Hown" as (l') "#[H↦b #Hown]".
     iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     iApply (wp_step_fupd _ (_∖_) with "[Hown Htok2]"); try done.
-    - iApply ("Hown" with "[%] Htok2"). set_solver+.
+    - iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
     - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
       iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
       iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
@@ -105,7 +105,7 @@ Section borrow.
     iIntros (Hκ Hincl tid) "#LFT #HE $ HL Hp".
     rewrite tctx_interp_singleton.
     iDestruct (Hincl with "HL HE") as "#Hincl".
-    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
+    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
     iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
@@ -137,15 +137,15 @@ Section borrow.
   Proof.
     iIntros (Hκ Hincl tid) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
     iDestruct (Hincl with "HL HE") as "#Hincl".
-    iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
+    iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
     iDestruct "Hshr" as (l') "[H↦ Hown]".
     iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
     iAssert (κ ⊑ κ' ⊓ κ)%I as "#Hincl'".
     { iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
-    iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
+    iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']"; first solve_ndisj.
     iApply (wp_step_fupd _ (_∖_) with "[Hown Htok2]"); try done.
-    - iApply ("Hown" with "[%] Htok2"). set_solver+.
+    - iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
     - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
       iMod ("Hclose''" with "Htok2") as "Htok2".
       iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 68d951e7..1f413f86 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -274,7 +274,7 @@ Section typing.
         rewrite /= left_id in EQ. subst κ'. simpl. wp_rec. wp_bind Endlft.
         iSpecialize ("Hinh" with "Htk").
         iApply (wp_mask_mono (↑lftN)); first done.
-        iApply (wp_step_fupd with "Hinh"); [set_solver+..|]. wp_seq.
+        iApply (wp_step_fupd with "Hinh"); [solve_ndisj..|]. wp_seq.
         iIntros "#Htok !>". wp_seq. iMod ("Hclose" with "Htok") as "HL".
         iSpecialize ("HC" with "[]"); first by (iPureIntro; apply elem_of_list_singleton).
         iApply ("HC" $! [#r] with "Htl HL").
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 632ef0a3..c3a9c6df 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -79,7 +79,7 @@ Section rc.
     set (C := (∃ _ _ _ _, _ ∗ _ ∗ _ ∗ &na{_,_,_} _ ∗ _)%I).
     iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
           with "[Hpbown]") as "#Hinv"; first by iLeft.
-    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose1]"; first set_solver.
+    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (&{κ} _)%I with "[Hbtok]" as "Hb".
       { rewrite bor_unfold_idx. iExists _. by iFrame. }
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 98a2abe3..029ec6d5 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -65,7 +65,7 @@ Section refmut.
     iExists _, _. iSplit.
     - by iApply frac_bor_shorten.
     - iIntros "!# * % Htok".
-      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
       { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
       iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
       iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
@@ -98,7 +98,7 @@ Section refmut.
       + by iApply lft_incl_trans.
     - iIntros (κ tid l) "H". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
       iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
-      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
       { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
       iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
       iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 7003099d..9da6cf50 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -54,7 +54,7 @@ Section rwlockwriteguard.
     iExists _. iSplit.
     - by iApply frac_bor_shorten.
     - iIntros "!# * % Htok".
-      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
       { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
       iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
       iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
@@ -94,7 +94,7 @@ Section rwlockwriteguard.
         iIntros "!>!#"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
     - iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
       iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
-      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
+      iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
       { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
       iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
       iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 8d01d9ad..5268ca38 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -68,22 +68,22 @@ Section own.
   Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
     move=>n ty N κ l tid ?? /=. iIntros "#LFT Hshr Htok".
-    iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
-    iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
+    iMod (bor_exists with "LFT Hshr") as (vl) "Hb"; first solve_ndisj.
+    iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj.
     destruct vl as [|[[|l'|]|][]];
-      try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[]_]"; set_solver).
+      try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[]_]"; solve_ndisj).
     iFrame. iExists l'. rewrite heap_mapsto_vec_singleton.
-    iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
-    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
+    iMod (bor_sep with "LFT Hb2") as "[Hb2 _]"; first solve_ndisj.
+    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
     iApply delay_sharing_later; done.
   Qed.
   Next Obligation.
     intros _ ty κ κ' tid l. iIntros "#Hκ #H".
     iDestruct "H" as (l') "[Hfb #Hvs]".
     iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!# *% Htok".
-    iApply (step_fupd_mask_mono F _ _ (F∖↑shrN)). set_solver. set_solver.
-    iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first set_solver.
-    iMod ("Hvs" with "[%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
+    iApply (step_fupd_mask_mono F _ _ (F∖↑shrN)); [solve_ndisj..|].
+    iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+    iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
     iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
     by iApply (ty.(ty_shr_mono) with "Hκ").
   Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index a51abc53..b93c3bd2 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -15,7 +15,7 @@ Section product.
   Global Instance unit0_copy : Copy unit0.
   Proof.
     split. by apply _. iIntros (????????) "_ _ Htok $".
-    iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
+    iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
     iExists 1%Qp. iModIntro. iSplitR.
     { iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto. }
     iIntros "Htok2 _". iApply "Htok". done.
@@ -57,9 +57,9 @@ Section product.
   Qed.
   Next Obligation.
     intros ty1 ty2 E κ l tid q ?. iIntros "#LFT /=H Htok". rewrite split_prod_mt.
-    iMod (bor_sep with "LFT H") as "[H1 H2]". set_solver.
-    iMod (ty1.(ty_share) with "LFT H1 Htok") as "[? Htok]". solve_ndisj.
-    iMod (ty2.(ty_share) with "LFT H2 Htok") as "[? Htok]". solve_ndisj.
+    iMod (bor_sep with "LFT H") as "[H1 H2]"; first solve_ndisj.
+    iMod (ty1.(ty_share) with "LFT H1 Htok") as "[? Htok]"; first solve_ndisj.
+    iMod (ty2.(ty_share) with "LFT H2 Htok") as "[? Htok]"; first solve_ndisj.
     iModIntro. iFrame "Htok". iFrame.
   Qed.
   Next Obligation.
@@ -104,9 +104,9 @@ Section product.
   Proof.
     split; first (intros; apply _).
     intros κ tid E F l q ? HF. iIntros "#LFT [H1 H2] Htl [Htok1 Htok2]".
-    iMod (@copy_shr_acc with "LFT H1 Htl Htok1") as (q1) "(Htl & H1 & Hclose1)"; first set_solver.
+    iMod (@copy_shr_acc with "LFT H1 Htl Htok1") as (q1) "(Htl & H1 & Hclose1)"; first solve_ndisj.
     { rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. omega. }
-    iMod (@copy_shr_acc with "LFT H2 Htl Htok2") as (q2) "(Htl & H2 & Hclose2)"; first set_solver.
+    iMod (@copy_shr_acc with "LFT H2 Htl Htok2") as (q2) "(Htl & H2 & Hclose2)"; first solve_ndisj.
     { move: HF. rewrite /= -plus_assoc shr_locsE_shift.
       assert (shr_locsE l (ty_size ty1) ⊥ shr_locsE (shift_loc l (ty_size ty1)) (ty_size ty2 + 1))
              by exact: shr_locsE_disj.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 4f54c80e..d2ca80bc 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -145,8 +145,8 @@ Section product_split.
     iIntros (tid q) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[Hp H]"; try done. iDestruct "Hp" as %Hp.
-    rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]".
-    set_solver. rewrite /tctx_elt_interp /=.
+    rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]"; first solve_ndisj.
+    rewrite /tctx_elt_interp /=.
     iSplitL "H1"; iExists _; (iSplitR; first by rewrite Hp); auto.
   Qed.
 
@@ -159,7 +159,7 @@ Section product_split.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1.
     iDestruct "Hp2" as %[=<-]. iExists #l. iFrame "%".
-    iMod (bor_combine with "LFT H1 H2") as "H". set_solver. by rewrite /= split_prod_mt.
+    iMod (bor_combine with "LFT H1 H2") as "H"; first solve_ndisj. by rewrite /= split_prod_mt.
   Qed.
 
   Lemma uniq_is_ptr κ ty tid (vl : list val) :
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 8d52bd5f..66e76ea8 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -81,10 +81,9 @@ Section typing.
   Proof.
     iIntros (Hcopy Halive) "!#".
     iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL #Hshr"; try done.
-    iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
-    assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. (* set_solver needs some help. *)
-    iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)".
-    { set_solver. } { rewrite ->shr_locsE_shrN. set_solver. }
+    iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
+    iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)"; first solve_ndisj.
+    { rewrite ->shr_locsE_shrN. solve_ndisj. }
     iDestruct "H↦" as (vl) "[>Hmt #Hown]". iModIntro. iExists _, _, _.
     iFrame "∗#". iSplit; first done. iIntros "Hmt".
     iMod ("Hcl" with "Htl [Hmt]") as "[$ Hκ]"; first by iExists _; iFrame.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 45048331..d3b4a77c 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -80,11 +80,11 @@ Section sum.
   Qed.
   Next Obligation.
     intros tyl E κ l tid. iIntros (??) "#LFT Hown Htok". rewrite split_sum_mt.
-    iMod (bor_exists with "LFT Hown") as (i) "Hown". set_solver.
-    iMod (bor_sep with "LFT Hown") as "[Hmt Hown]". solve_ndisj.
+    iMod (bor_exists with "LFT Hown") as (i) "Hown"; first solve_ndisj.
+    iMod (bor_sep with "LFT Hown") as "[Hmt Hown]"; first solve_ndisj.
     iMod ((nth i tyl ∅).(ty_share) with "LFT Hown Htok") as "[#Hshr $]"; try done.
-    iMod (bor_fracture with "LFT [Hmt]") as "H'";[set_solver| |]; last eauto.
-      by iFrame.
+    iMod (bor_fracture with "LFT [Hmt]") as "H'"; first solve_ndisj; last eauto.
+    by iFrame.
   Qed.
   Next Obligation.
     iIntros (tyl κ κ' tid l) "#Hord H".
@@ -204,7 +204,7 @@ Section sum.
     - intros κ tid E F l q ? HF.
       iIntros "#LFT #H Htl [Htok1 Htok2]".
       setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
-      iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[>Hown Hclose]". set_solver.
+      iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[>Hown Hclose]"; first solve_ndisj.
       iAssert ((∃ vl, is_pad i tyl vl)%I) with "[#]" as %[vl Hpad].
       { iDestruct "Hown" as "[_ Hpad]". iDestruct "Hpad" as (vl) "[_ %]".
         eauto. }
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 0e8fdeae..946c9486 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -128,9 +128,9 @@ Program Definition ty_of_st `{typeG Σ} (st : simple_type) : type :=
 Next Obligation. intros. apply st_size_eq. Qed.
 Next Obligation.
   iIntros (?? st E κ l tid ??) "#LFT Hmt Hκ".
-  iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
-  iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
-  iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]". set_solver.
+  iMod (bor_exists with "LFT Hmt") as (vl) "Hmt"; first solve_ndisj.
+  iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]"; first solve_ndisj.
+  iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]"; first solve_ndisj.
   - iFrame "Hκ".
     iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
   - iExFalso. by iApply (lft_tok_dead with "Hκ").
@@ -485,9 +485,9 @@ Section type.
   Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
   Next Obligation.
     iIntros (st κ tid E ? l q ? HF) "#LFT #Hshr Htok Hlft".
-    iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
+    iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
     iDestruct "Hshr" as (vl) "[Hf Hown]".
-    iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
+    iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first solve_ndisj.
     iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]".
     iSplitL "Hmt1"; first by auto with iFrame.
     iIntros "Htok2 Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index e8f07a2d..f7c20257 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -23,11 +23,11 @@ Section uniq_bor.
   Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
     move=> κ ty N κ' l tid ??/=. iIntros "#LFT Hshr Htok".
-    iMod (bor_exists with "LFT Hshr") as ([|[[|l'|]|][]]) "Hb"; first set_solver;
-      (iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first set_solver);
-      try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[] _]"; set_solver).
+    iMod (bor_exists with "LFT Hshr") as ([|[[|l'|]|][]]) "Hb"; first solve_ndisj;
+      (iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj);
+      try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[] _]"; solve_ndisj).
     iFrame. iExists l'. subst. rewrite heap_mapsto_vec_singleton.
-    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
+    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
     iApply delay_sharing_nested; try done. iApply lft_incl_refl.
   Qed.
   Next Obligation.
@@ -36,9 +36,9 @@ Section uniq_bor.
     { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
     iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
     iIntros "!# * % Htok".
-    iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)); try set_solver.
-    iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first set_solver.
-    iMod ("Hvs" with "[%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
+    iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)); try solve_ndisj.
+    iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
+    iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
     iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
     by iApply (ty_shr_mono with "Hκ0").
   Qed.
@@ -61,7 +61,7 @@ Section uniq_bor.
     - iIntros (κ ??) "H". iAssert (κ2 ⊓ κ ⊑ κ1 ⊓ κ)%I as "#Hincl'".
       { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
       iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!# %%% Htok".
-      iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first set_solver.
+      iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
       iMod ("Hupd" with "[%] Htok") as "Hupd'"; try done. iModIntro. iNext.
       iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
       iApply ty_shr_mono; [done..|]. by iApply "Hs".
@@ -177,8 +177,8 @@ Section typing.
   Proof.
     iIntros (Hcopy Halive) "!#".
     iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL Hown"; try done.
-    iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
-    iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first set_solver.
+    iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
+    iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first solve_ndisj.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%". iIntros "!>".
     iExists _, _, _. iSplit; first done. iFrame "∗#". iIntros "H↦".
@@ -191,8 +191,8 @@ Section typing.
   Proof.
     iIntros (Halive) "!#".
     iIntros ([[]|] tid F qL ?) "#LFT HE HL Hown"; try done.
-    iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
-    iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']". set_solver.
+    iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
+    iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']"; first solve_ndisj.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
     iDestruct "Hown" as ">%". iModIntro. iExists _, _. iSplit; first done.
     iFrame. iIntros "Hown". iDestruct "Hown" as (vl') "[H↦ Hown]".
diff --git a/theories/typing/util.v b/theories/typing/util.v
index fc3e279d..784d9ad5 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -32,14 +32,14 @@ Section util.
     iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
     iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ tid l)%I
           with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first set_solver.
+    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hdelay"; first solve_ndisj.
       { rewrite bor_unfold_idx. eauto. }
       iModIntro. iNext. iMod "Hdelay" as "[Hb Htok]".
       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.
+    - iMod fupd_intro_mask' as "Hclose'"; first solve_ndisj. iModIntro.
       iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
 
@@ -53,15 +53,15 @@ Section util.
     iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
     iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ'' tid l)%I
           with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first set_solver.
+    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_unnest with "LFT [Hbtok]") as "Hb". solve_ndisj.
+    - iMod (bor_unnest with "LFT [Hbtok]") as "Hb"; first solve_ndisj.
       { iApply bor_unfold_idx. eauto. }
       iModIntro. iNext. iMod "Hb".
-      iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
+      iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]"; first solve_ndisj.
       { iApply bor_shorten; done. }
       iMod ("Hclose" with "[]") as "_"; auto.
-    - iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
+    - iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first solve_ndisj.
       iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
 End util.
-- 
GitLab