diff --git a/tests/bitvector_tactics.v b/tests/bitvector_tactics.v
index 4b371b3a429a6b48f0e108f72782e772cd7ca5b5..46fda5c1c7bb38e0d7f05d7d972961d489fb6634 100644
--- a/tests/bitvector_tactics.v
+++ b/tests/bitvector_tactics.v
@@ -13,7 +13,7 @@ Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
 Goal ∀ a : Z, Z_to_bv 64 a `+Z` 1 = Z_to_bv 64 (Z.succ a).
 Proof.
   intros. bv_simplify. Show.
-  Restart.
+Restart. Proof.
   intros. bv_solve.
 Qed.
 
@@ -26,7 +26,7 @@ Goal ∀ l r xs : bv 64, ∀ data : list (bv 64),
                        bv_extract 0 64 (bv_zero_extend 128 ((r - l) ≫ 1))) * 8) < 2 ^ 52.
 Proof.
   intros. bv_simplify_arith. Show.
-  Restart.
+Restart. Proof.
   intros. bv_solve.
 Qed.
 
@@ -40,7 +40,7 @@ Goal ∀ l r : bv 64, ∀ data : list (bv 64),
 Proof.
   intros. bv_simplify_arith select (¬ _ >= _). bv_simplify_arith.
   split. (* We need to split since the [_ < _ ≤ _] notation differs between Coq versions. *) Show.
-  Restart.
+Restart. Proof.
   intros. bv_simplify_arith select (¬ _ >= _). bv_solve.
 Qed.
 
@@ -50,7 +50,7 @@ Goal ∀ r1 : bv 64,
   bv_extract 0 64 (bv_zero_extend 128 r1 + 0xffffffffffffffe9 + 1) ≠ 0.
 Proof.
   intros. bv_simplify. Show.
-  Restart.
+Restart. Proof.
   intros. bv_solve.
 Qed.
 
@@ -62,7 +62,7 @@ Goal ∀ i n : bv 64,
   bv_unsigned (bv_extract 0 64 (bv_zero_extend 128 i) + 1) < bv_unsigned n.
 Proof.
   intros. bv_simplify_arith select (bv_extract _ _ _ ≠ _). bv_simplify. Show.
-  Restart.
+Restart. Proof.
   intros. bv_simplify_arith select (bv_extract _ _ _ ≠ _). bv_solve.
 Qed.
 
@@ -76,9 +76,18 @@ Qed.
 
 (** Regression test for https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/411 *)
 Goal ∀ b : bv 16, bv_wrap 16 (bv_unsigned b) = bv_wrap 16 (bv_unsigned b).
-Proof. intros. bv_simplify. Show. Restart. intros. bv_solve. Qed.
+Proof.
+  intros. bv_simplify. Show.
+Restart. Proof.
+  intros. bv_solve.
+Qed.
 Goal ∀ b : bv 16, bv_wrap 16 (bv_unsigned b) ≠ bv_wrap 16 (bv_unsigned (b + 1)).
-Proof. intros. bv_simplify. Show. Restart. intros. bv_solve. Qed.
+Proof.
+  intros. bv_simplify. Show.
+Restart. Proof.
+  intros. bv_solve.
+Qed.
+
 Goal ∀ b : bv 16, bv_unsigned b = bv_unsigned b → True.
 Proof. intros ? H. bv_simplify H. Show. Abort.
 Goal ∀ b : bv 16, bv_unsigned b ≠ bv_unsigned (b + 1) → True.
diff --git a/tests/proper.v b/tests/proper.v
index 950b11d96f653ce761564a808e13ddf3765cc135..7b334e31422b0c8928175fe6647457e14b9b3112 100644
--- a/tests/proper.v
+++ b/tests/proper.v
@@ -18,38 +18,74 @@ Section map_tests.
   Global Instance map_alter_proper_test (f : A → A) i :
     Proper ((≡) ==> (≡)) f →
     Proper ((≡) ==> (≡)) (alter (M:=M A) f i).
-  Proof. apply _. Restart. solve_proper. Abort.
+  Proof.
+    apply _.
+  Restart. Proof.
+    solve_proper.
+  Abort.
   Global Instance map_zip_proper_test `{Equiv B} :
     Proper ((≡@{M A}) ==> (≡@{M B}) ==> (≡@{M (A * B)})) map_zip.
-  Proof. apply _. Restart. solve_proper. Abort.
+  Proof.
+    apply _.
+  Restart. Proof.
+    solve_proper.
+  Abort.
   Global Instance map_zip_with_proper_test `{Equiv B, Equiv C} (f : A → B → C) :
     Proper ((≡) ==> (≡) ==> (≡)) f →
     Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
-  Proof. apply _. Restart. solve_proper. Abort.
+  Proof.
+    apply _.
+  Restart. Proof.
+    solve_proper.
+  Abort.
   Global Instance map_fmap_proper_test `{Equiv B} (f : A → B) :
     Proper ((≡) ==> (≡)) f →
     Proper ((≡) ==> (≡@{M _})) (fmap f).
-  Proof. apply _. Restart. solve_proper. Abort.
+  Proof.
+    apply _.
+  Restart. Proof.
+    solve_proper.
+  Abort.
   Global Instance map_omap_proper_test `{Equiv B} (f : A → option B) :
     Proper ((≡) ==> (≡)) f →
     Proper ((≡) ==> (≡@{M _})) (omap f).
-  Proof. apply _. Restart. solve_proper. Abort.
+  Proof.
+    apply _.
+  Restart. Proof.
+    solve_proper.
+  Abort.
 End map_tests.
 
 (** And similarly for lists *)
 Global Instance list_alter_proper_test `{!Equiv A} (f : A → A) i :
   Proper ((≡) ==> (≡)) f →
   Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
-Proof. apply _. Restart. solve_proper. Abort.
+Proof.
+  apply _.
+Restart. Proof.
+  solve_proper.
+Abort.
 Global Instance list_fmap_proper_test `{!Equiv A, !Equiv B} (f : A → B) :
   Proper ((≡) ==> (≡)) f → Proper ((≡@{list A}) ==> (≡)) (fmap f).
-Proof. apply _. Restart. solve_proper. Abort.
+Proof.
+  apply _.
+Restart. Proof.
+  solve_proper.
+Abort.
 Global Instance list_bind_proper_test `{!Equiv A, !Equiv B} (f : A → list B) :
   Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mbind f).
-Proof. apply _. Restart. solve_proper. Abort.
+Proof.
+  apply _.
+Restart. Proof.
+  solve_proper.
+Abort.
 Global Instance mapM_proper_test `{!Equiv A, !Equiv B} (f : A → option B) :
   Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mapM f).
-Proof. apply _. Restart. solve_proper. Abort.
+Proof.
+  apply _.
+Restart. Proof.
+  solve_proper.
+Abort.
 
 Lemma test_prod_equivalence (X1 X2 X3 Y : propset nat * propset nat) :
   X3 ≡ X2 → X2 ≡ X1 → (X1,Y) ≡ (X3,Y).
diff --git a/tests/sets.v b/tests/sets.v
index caafd4c2568ce601a67022b98898438b11ce7253..7513db44b0c50c6a8de404db1df56e0e49154cff 100644
--- a/tests/sets.v
+++ b/tests/sets.v
@@ -25,7 +25,7 @@ Lemma set_guard_case_guard `{MonadSet M} `{Decision P} A (x : A) (X : M A) :
 Proof.
   (* Test that [case_guard] works for sets and indeed generates two goals *)
   case_guard; [set_solver|set_solver].
-Restart.
+Restart. Proof.
   (* Test that [set_solver] supports [guard]. *)
   set_solver.
 Qed.
diff --git a/tests/tactics.v b/tests/tactics.v
index 847bf3b994c7aaab0b1c47327ef1530dd20ec1ce..2e755290c691f7bff55d13cc26b7e2bf37b9c9bd 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -59,14 +59,14 @@ Qed.
 Goal ∀ n : nat, match n with | 0 => n = 0 | S n' => n = S n' end.
 Proof.
   intros. by case_match.
-Restart.
+Restart. Proof.
   intros. by case_match eqn:Heq; revert Heq. (* [revert Heq] checks that [Heq] exists *)
 Qed.
 
 Goal ∀ n m : nat, match n with | 0 => m = 0 | S n' => m = S n' end → n = m.
 Proof.
   intros. by case_match.
-Restart.
+Restart. Proof.
   intros. by case_match eqn:Heq; revert Heq. (* [revert Heq] checks that [Heq] exists *)
 Qed.
 
@@ -82,27 +82,27 @@ Proof.
   intros P Q ??.
   (* should select the last hypothesis *)
   destruct select (_ ∨ _); by constructor.
-Restart.
+Restart. Proof.
   intros P Q ??.
   (* should select the last hypothesis *)
   destruct select (_ ∨ _) as [H1|H2].
   - right. exact H1.
   - left. exact H2.
-Restart.
+Restart. Proof.
   intros P Q ??.
   (* should select the last hypothesis *)
   inv select (_ ∨ _); by constructor.
-Restart.
+Restart. Proof.
   intros P Q ??.
   (* should select the last hypothesis *)
   inv select (_ ∨ _) as [H1|H2].
   - right. exact H1.
   - left. exact H2.
-Restart.
+Restart. Proof.
   intros P Q ??.
   (* should select the last hypothesis *)
   inversion select (_ ∨ _); by constructor.
-Restart.
+Restart. Proof.
   intros P Q ??.
   (* should select the last hypothesis *)
   inversion select (_ ∨ _) as [H1|H2].
@@ -148,7 +148,7 @@ Proof.
   (* Make sure we do the same thing as [inversion_clear] when there are
   other hypotheses before the one we invert. *)
   inversion_clear 2 as [|? H']. Show.
-Restart.
+Restart. Proof.
   inv 2 as [|? H']. Show. done.
 Qed.
 
@@ -167,36 +167,36 @@ Proof.
   huge and we don't want to specify it. What do we do? The "o" family of tactics
   for working with "o"pen terms helps. *)
   opose proof (HPQR1 _ (S _) _ _) as HR; [exact HP1|exact HQ|]. exact HR.
-Restart.
+Restart. Proof.
   (** We can have fewer [_]. *)
   opose proof (HPQR1 _ (S _) _) as HR; [exact HP1|]. exact (HR HQ).
-Restart.
+Restart. Proof.
   (** And even fewer. *)
   opose proof (HPQR1 _ (S _)) as HR. exact (HR HP1 HQ).
-Restart.
+Restart. Proof.
   (** The [*] variant automatically adds [_]. *)
   opose proof* (HPQR1 _ (S _)) as HR; [exact HP1|exact HQ|]. exact HR.
-Restart.
+Restart. Proof.
   (** Same deal for [generalize]. *)
   ogeneralize (HPQR1 _ 1). intros HR. exact (HR HP1 HQ).
-Restart.
+Restart. Proof.
   ogeneralize (HPQR1 _ 1 _); [exact HP1|]. intros HR. exact (HR HQ).
-Restart.
+Restart. Proof.
   ogeneralize* (HPQR1 _ 1); [exact HP1|exact HQ|]. intros HR. exact HR.
-Restart.
+Restart. Proof.
   (** [odestruct] also automatically adds subgoals until there is something
   to destruct, as usual. Note that [edestruct] wouldn't help here,
   it just complains that it cannot infer the placeholder. *)
   Fail edestruct (HPQR2 _ 1).
   odestruct (HPQR2 _ 1) as [HR1 HR2]; [exact HP1|exact HQ|]. exact HR1.
-Restart.
+Restart. Proof.
   (** [ospecialize] is like [opose proof] but it reuses the name.
   It only works on local assumptions. *)
   Fail ospecialize (plus 0 0).
   ospecialize (HPQR1 _ 1 _); [exact HP1|]. exact (HPQR1 HQ).
-Restart.
+Restart. Proof.
   ospecialize (HPQR1 _ 1). exact (HPQR1 HP1 HQ).
-Restart.
+Restart. Proof.
   ospecialize* (HPQR1 _ 1); [exact HP1|exact HQ|]. exact HPQR1.
 Qed.
 
@@ -206,7 +206,7 @@ Lemma o_tactic_with_forall (P Q R : nat → Prop) :
 Proof.
   intros HP HQ HR.
   ospecialize* HR; [exact HP|exact HQ|exact HR].
-Restart.
+Restart. Proof.
   intros HP HQ HR.
   opose proof* HR as HR'; [exact HP|exact HQ|exact HR'].
 Qed.
@@ -223,7 +223,7 @@ Check "oinv_test2".
 Lemma oinv_test2 n : even (2 + n) → even n.
 Proof.
   intros H. oinv H as [|? H']. Show. done.
-Restart.
+Restart. Proof.
   oinv 1 as [|? H']. Show. done.
 Qed.
 Lemma oinv_test_num (P : Prop) n :
@@ -276,7 +276,7 @@ Section f_equiv.
   Proof.
     (* The Coq tactic prefers the ⊆. *)
     intros. Morphisms.f_equiv. Fail assumption.
-  Restart.
+  Restart. Proof.
     intros. f_equiv. assumption.
   Qed.
 End f_equiv.