diff --git a/tests/algebra.v b/tests/algebra.v
index e62e613f8c194a63ad547d9515250636fd0c50bb..68cc8177c0e436362083a7f2902bbf0778c7b62c 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Import auth excl lib.gmap_view.
 From iris.base_logic.lib Require Import invariants.
+From iris.prelude Require Import options.
 
 Section test_dist_equiv_mode.
   (* check that the mode for [Dist] does not trigger https://github.com/coq/coq/issues/14441.
diff --git a/tests/atomic.v b/tests/atomic.v
index b36f9b636a3fddd6b63eefc4b89009301d4a1bc7..fc69d02d080379a2290a37de9737e6cd345e21d4 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index dfabf4c10ea95893ec2ea7a86ed8e5e016036c38..da4831eb227392734bf0602bc15cfe6e4d974861 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
 From iris.heap_lang Require Import lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -196,7 +196,7 @@ Section tests.
     val_is_unboxed v â†’
     l â†¦ v -âˆ— WP CmpXchg #l v v {{ _, True }}.
   Proof.
-    iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
+    iIntros (?) "?". wp_cmpxchg as ? | ?; done.
   Qed.
 
   Lemma wp_xchg l (vâ‚ vâ‚‚ : val) :
@@ -478,5 +478,6 @@ Section error_tests.
   Abort.
 End error_tests.
 
+(* Test a closed proof *)
 Lemma heap_e_adequate Ïƒ : adequate NotStuck heap_e Ïƒ (Î» v _, v = #2).
 Proof. eapply (heap_adequacy heapÎ£)=> ?. iIntros "_". by iApply heap_e_spec. Qed.
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index 8d72a987c7b91b5ba485b930ccc27cd159d6efa8..a4b12e368b056c0242b0b80707320beff339d5f3 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -3,7 +3,7 @@ printing *)
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
index 4d8e5f234aca1beb04ff1d355b0ad53120c6d11c..cb9db7b851ca3acc61fb4972af219d313caa0fcc 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -1,7 +1,6 @@
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
-From iris.heap_lang Require Import lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Section tests.
   Context `{!heapGS Î£}.
@@ -16,7 +15,14 @@ Section tests.
   Proof.
     iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
     wp_cmpxchg_suc. iIntros "!>" (ws ->) "Hp". eauto with iFrame.
-  Restart.
+  Qed.
+
+  Lemma test_resolve1' E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
+    l â†¦ #n -âˆ—
+    proph p vs -âˆ—
+    WP Resolve (CmpXchg #l #n (#n + #1)) #p v @ E
+      {{ v, âŒœv = (#n, #true)%VâŒ âˆ— âˆƒvs, proph p vs âˆ— l â†¦ #(n+1) }}.
+  Proof.
     iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve_cmpxchg_suc with "[$Hp $Hl]"); first by left.
     iIntros "Hpost". iDestruct "Hpost" as (ws ->) "Hp". eauto with iFrame.
   Qed.
diff --git a/tests/heapprop.v b/tests/heapprop.v
index 9f2b36e044871126f31bdcb4e16d402d2f3d367a..de2eaa478f72dab7fab448d322cfd1e385d35a22 100644
--- a/tests/heapprop.v
+++ b/tests/heapprop.v
@@ -1,6 +1,7 @@
 From stdpp Require Import gmap.
 From iris.bi Require Import interface.
 From iris.proofmode Require Import tactics.
+From iris.prelude Require Import options.
 
 (** This file constructs a simple non step-indexed linear separation logic as
 predicates over heaps (modeled as maps from integer locations to integer values).
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index d7ba9448abfccedb64306a3210c46f8a8568b2ab..ffb9ec7401e0669317d36ddfd8ae57d7c7505a14 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -14,7 +14,7 @@
   --------------------------------------âˆ—
   Î¨ x âˆ— P
   
-2 goals
+1 goal
   
   M : ucmra
   A : Type
@@ -26,13 +26,6 @@
   --------------------------------------âˆ—
   Î¨ x
   
-
-goal 2 is:
- "HP" : P
-"HR" : R
---------------------------------------âˆ—
-P
-
 1 goal
   
   M : ucmra
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 24abfeda8ba64783e25a2dc74f200f6e928a0129..3bc0914b39d9b9fd2cd5d40449874c5429fcaa04 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -7,7 +7,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import base_logic.
 From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -23,7 +23,9 @@ Section demo.
     intros [HP [HÎ¨ HR]].
     destruct HÎ¨ as [x HÎ¨].
     exists x.
-    split. assumption. assumption.
+    split.
+    -  assumption.
+    -  assumption.
   Qed.
 
   (* The version in IPM *)
@@ -34,7 +36,9 @@ Section demo.
     iIntros "[HP [HÎ¨ HR]]".
     iDestruct "HÎ¨" as (x) "HÎ¨".
     iExists x. Show.
-    iSplitL "HÎ¨". Show. iAssumption. Show. iAssumption.
+    iSplitL "HÎ¨".
+    - Show. iAssumption.
+    - Show. iAssumption.
   Qed.
 
   (* The short version in IPM, as in the paper *)
@@ -174,7 +178,7 @@ Section M.
   Global Instance frag_core_id n : CoreId (Frag n).
   Proof. by constructor. Qed.
   Lemma auth_frag_valid j n : âœ“ (Auth n â‹… Frag j) â†’ j â‰¤ n.
-  Proof. simpl. case_decide. done. by intros []. Qed.
+  Proof. simpl. case_decide; first done. by intros []. Qed.
   Lemma auth_frag_op (j n : nat) : j â‰¤ n â†’ Auth n = Auth n â‹… Frag j.
   Proof. intros. by rewrite /= decide_True. Qed.
 
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 04d426610523bf78984a3bcde83827f6a6f09759..4f98fa49048928f410a04ae435eb560ac6000fec 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Export tactics.
 From iris.program_logic Require Export total_weakestpre weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/mosel_paper.v b/tests/mosel_paper.v
index 00a84f31f2a30d28bdb9869cb64f76097181d287..ed19935dde47f30b26817cae2f7529b47e2b7f28 100644
--- a/tests/mosel_paper.v
+++ b/tests/mosel_paper.v
@@ -7,6 +7,7 @@ Jan-Oliver Kaiser, Amin Timany, Arthur CharguÃ©raud, Derek Dreyer
 ICFP 2018 *)
 From iris.bi Require Import monpred.
 From iris.proofmode Require Import tactics monpred.
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 12ac80df3a2df7ad270200c821b1f777016a15dd..c5ca6dbb9359c34f1775c1a1866f039a7a5e948b 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -5,7 +5,7 @@ From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
 From iris.heap_lang.lib Require Import par.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 (** This is the introductory example from the "Iris from the Ground Up" journal
 paper. *)
@@ -76,8 +76,12 @@ Proof.
     iAssert (one_shot_inv Î³ l âˆ— (âŒœv = NONEVâŒ âˆ¨ âˆƒ n : Z,
       âŒœv = SOMEV #nâŒ âˆ— own Î³ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
-      + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
-      + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
+      + Show. iSplit.
+        * iLeft; by iSplitL "Hl".
+        * eauto.
+      + iSplit.
+        * iRight; iExists m; by iSplitL "Hl".
+        * eauto. }
     iSplitL "Hinv"; first by eauto.
     iModIntro. wp_pures. iIntros "!> !>". wp_lam.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% HÎ³']";
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 5a23af9f5332fb45b30bdc334aabf9fb1b54f90c..7df7a238444dc0711c48649a572768e239a39464 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -5,7 +5,7 @@ From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
 From iris.heap_lang.lib Require Import par.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 (** This is the introductory example from Ralf's PhD thesis.
 The difference to [one_shot] is that [set] asserts to be called only once. *)
@@ -92,8 +92,12 @@ Proof.
     iAssert (one_shot_inv Î³ l âˆ— (âŒœv = NONEVâŒ âˆ¨ âˆƒ n : Z,
       âŒœv = SOMEV #nâŒ âˆ— own Î³ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
-      + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
-      + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
+      + Show. iSplit.
+        * iLeft; by iSplitL "Hl".
+        * eauto.
+      + iSplit.
+        * iRight; iExists m; by iSplitL "Hl".
+        * eauto. }
     iSplitL "Hinv"; first by eauto.
     iModIntro. wp_pures. iIntros "!> !>". wp_lam. wp_bind (! _)%E.
     iInv N as "Hinv".
diff --git a/tests/proofmode.v b/tests/proofmode.v
index afcfd89f24e1c9f6aa25391448e8fe50fe7e6c51..03b44f242cce64a05a09000da3b14566dd5e92b6 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,6 +1,6 @@
 From iris.bi Require Import laterable.
 From iris.proofmode Require Import tactics intro_patterns.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -28,7 +28,7 @@ Proof.
   (* should remove the disjunction "H" *)
   iDestruct "H" as "[#?|#?]"; last by iLeft. Show.
   (* should keep the disjunction "H" because it is instantiated *)
-  iDestruct ("H2" $! 10) as "[%|%]". done. done.
+  iDestruct ("H2" $! 10) as "[%|%]"; done.
 Qed.
 
 Lemma demo_2 P1 P2 P3 P4 Q (P5 : nat â†’ PROP) `{!Affine P4, !Absorbing P2} :
@@ -46,7 +46,7 @@ Proof.
   (* split takes a list of hypotheses just for the LHS *)
   iSplitL "H3".
   - iFrame "H3". iRight. auto.
-  - iSplitL "HQ". iAssumption. by iSplitL "H1".
+  - iSplitL "HQ"; first iAssumption. by iSplitL "H1".
 Qed.
 
 Lemma demo_3 P1 P2 P3 :
@@ -719,7 +719,11 @@ Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
 
 Lemma test_iAlways P Q R :
   â–¡ P -âˆ— <pers> Q â†’ R -âˆ— <pers> <affine> <affine> P âˆ— â–¡ Q.
-Proof. iIntros "#HP #HQ HR". iSplitL. iModIntro. done. iModIntro. done. Qed.
+Proof.
+  iIntros "#HP #HQ HR". iSplitL.
+  - iModIntro. done.
+  - iModIntro. done.
+Qed.
 
 (* A bunch of test cases from #127 to establish that tactics behave the same on
 `âŒœ Ï† âŒ â†’ P` and `âˆ€ _ : Ï†, P` *)
@@ -731,7 +735,7 @@ Lemma test_forall_nondep_2 (Ï† : Prop) :
 Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" with "[% //]"). done. Qed.
 Lemma test_forall_nondep_3 (Ï† : Prop) :
   Ï† â†’ (âˆ€ _ : Ï†, False : PROP) -âˆ— False.
-Proof. iIntros (HÏ†) "HÏ†". unshelve iSpecialize ("HÏ†" $! _). done. done. Qed.
+Proof. iIntros (HÏ†) "HÏ†". unshelve iSpecialize ("HÏ†" $! _); done. Qed.
 Lemma test_forall_nondep_4 (Ï† : Prop) :
   Ï† â†’ (âˆ€ _ : Ï†, False : PROP) -âˆ— False.
 Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" $! HÏ†); done. Qed.
@@ -744,7 +748,7 @@ Lemma test_pure_impl_2 (Ï† : Prop) :
 Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" with "[% //]"). done. Qed.
 Lemma test_pure_impl_3 (Ï† : Prop) :
   Ï† â†’ (âŒœÏ†âŒ â†’ False : PROP) -âˆ— False.
-Proof. iIntros (HÏ†) "HÏ†". unshelve iSpecialize ("HÏ†" $! _). done. done. Qed.
+Proof. iIntros (HÏ†) "HÏ†". unshelve iSpecialize ("HÏ†" $! _); done. Qed.
 Lemma test_pure_impl_4 (Ï† : Prop) :
   Ï† â†’ (âŒœÏ†âŒ â†’ False : PROP) -âˆ— False.
 Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" $! HÏ†). done. Qed.
@@ -901,24 +905,32 @@ Qed.
 Lemma iFrame_with_evar_r P Q :
   âˆƒ R, (P -âˆ— Q -âˆ— P âˆ— R) âˆ§ R = Q.
 Proof.
-  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
+  eexists. split.
+  - iIntros "HP HQ". iFrame. iApply "HQ".
+  - done.
 Qed.
 Lemma iFrame_with_evar_l P Q :
   âˆƒ R, (P -âˆ— Q -âˆ— R âˆ— P) âˆ§ R = Q.
 Proof.
-  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
-  iSplitR "HP"; iAssumption. done.
+  eexists. split.
+  - iIntros "HP HQ". Fail iFrame "HQ".
+    iSplitR "HP"; iAssumption.
+  - done.
 Qed.
 Lemma iFrame_with_evar_persistent P Q :
   âˆƒ R, (P -âˆ— â–¡ Q -âˆ— P âˆ— R âˆ— Q) âˆ§ R = emp%I.
 Proof.
-  eexists. split. iIntros "HP #HQ". iFrame "HQ HP". iEmpIntro. done.
+  eexists. split.
+  - iIntros "HP #HQ". iFrame "HQ HP". iEmpIntro.
+  - done.
 Qed.
 
 Lemma test_iAccu P Q R S :
   âˆƒ PP, (â–¡P -âˆ— Q -âˆ— R -âˆ— S -âˆ— PP) âˆ§ PP = (Q âˆ— R âˆ— S)%I.
 Proof.
-  eexists. split. iIntros "#? ? ? ?". iAccu. done.
+  eexists. split.
+  - iIntros "#? ? ? ?". iAccu.
+  - done.
 Qed.
 
 Lemma test_iAssumption_evar P : âˆƒ R, (R âŠ¢ P) âˆ§ R = P.
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index fa04cc2a565bef12c094e298bef37cf7df39dea4..f7f4d6021b582916b3a3b11f5e2dd84985c22bbc 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -1,10 +1,10 @@
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
+From iris.prelude Require Import options.
 
 From iris.bi Require Import ascii.
 
-Set Default Proof Using "Type".
 Unset Mangle Names.
 
 (* Remove this and the [Set Printing Raw Literals.] below once we require Coq
@@ -36,7 +36,7 @@ Section base_logic_tests.
     iExists (S j + z1), z2.
     iNext.
     iApply ("H3" $! _ 0 with "[$]").
-    - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
+    - iSplit; first done. iApply "H2". iLeft. iApply "H2". by iRight.
     - done.
   Qed.
 
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 955fb532c1aa07f7f6579c30686cd0b9cc9a1cb7..5bfe65ba248c77dcc2c09b636433ff1a67a78cad 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -2,6 +2,7 @@ From iris.algebra Require Import frac.
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -30,7 +31,7 @@ Section base_logic_tests.
     iExists (S j + z1), z2.
     iNext.
     iApply ("H3" $! _ 0 with "[$]").
-    - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
+    - iSplit; first done. iApply "H2". iLeft. iApply "H2". by iRight.
     - done.
   Qed.
 
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 990f81f2a64469f1e88aed418dfb565fe3edc7ba..66d9f61aaaa6b7d1bd15741c6977feb067669651 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic.lib Require Import invariants.
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/proofmode_siprop.v b/tests/proofmode_siprop.v
index 57e9a7332d47f12831d65ad23665ae0fb8eb953b..3e3efcc049bed9be966a20d551836aebacb4aae7 100644
--- a/tests/proofmode_siprop.v
+++ b/tests/proofmode_siprop.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.si_logic Require Import bi.
+From iris.prelude Require Import options.
 
 Section si_logic_tests.
   Implicit Types P Q R : siProp.
diff --git a/tests/string_ident.v b/tests/string_ident.v
index 6de14c131a30ca84cbf538d5ba5b7da36ae9abb9..dc22df6de751ac4f66c2f003313a062f3ba7889c 100644
--- a/tests/string_ident.v
+++ b/tests/string_ident.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import string_ident.
 From Coq Require Import Strings.String.
 From stdpp Require Import base.
-Open Scope string.
+Local Open Scope string.
 
 Lemma test_basic_ident : âˆ€ (n:nat), n = n.
 Proof.
diff --git a/tests/telescopes.v b/tests/telescopes.v
index ce3a0290bed7f37916962052dce8c9e86d350520..1e7fcc3e5d5bf394bad657d4615411b924b024ba 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -1,6 +1,6 @@
 From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index 7f830cba20792efd502a46652a9cb74848ece660..b5683256d0d2dd0652c28a8dbca44e129abc4038 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Export tactics.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Inductive tree :=
   | leaf : Z â†’ tree