diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index f1abfea776bb17fa5c38e19e9571bbdd0e36e1d8..7481a1a6d3874b4d2ea81bf0c22681d1999bf87d 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -59,7 +59,7 @@ Proof. rewrite envs_entails_eq=> ? ->. by apply twp_value. Qed.
 
 Ltac wp_value_head :=
   first [eapply tac_wp_value || eapply tac_twp_value];
-    [apply _
+    [iSolveTC
     |iEval (lazy beta; simpl of_val)].
 
 Tactic Notation "wp_pure" open_constr(efoc) :=
@@ -70,9 +70,9 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     reshape_expr e ltac:(fun K e' =>
       unify e' efoc;
       eapply (tac_wp_pure _ _ _ _ (fill K e'));
-      [apply _                        (* PureExec *)
+      [iSolveTC                       (* PureExec *)
       |try fast_done                  (* The pure condition for PureExec *)
-      |apply _                        (* IntoLaters *)
+      |iSolveTC                       (* IntoLaters *)
       |wp_expr_simpl_subst; try wp_value_head (* new goal *)
       ])
     || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
@@ -81,7 +81,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     reshape_expr e ltac:(fun K e' =>
       unify e' efoc;
       eapply (tac_twp_pure _ _ _ (fill K e'));
-      [apply _                        (* PureExec *)
+      [iSolveTC                       (* PureExec *)
       |try fast_done                  (* The pure condition for PureExec *)
       |wp_expr_simpl_subst; try wp_value_head (* new goal *)
       ])
@@ -325,14 +325,14 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..])
+         eapply (tac_wp_alloc _ _ _ _ H K); [iSolveTC|..])
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
-    [apply _
+    [iSolveTC
     |finish ()]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_alloc _ _ _ H K); [apply _|..])
+         eapply (tac_twp_alloc _ _ _ H K); [iSolveTC|..])
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
     finish ()
   | _ => fail "wp_alloc: not a 'wp'"
@@ -351,7 +351,7 @@ Tactic Notation "wp_load" :=
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
       |fail 1 "wp_load: cannot find 'Load' in" e];
-    [apply _
+    [iSolveTC
     |solve_mapsto ()
     |wp_expr_simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
@@ -374,16 +374,16 @@ Tactic Notation "wp_store" :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_store _ _ _ _ _ _ K); [apply _|..])
+         eapply (tac_wp_store _ _ _ _ _ _ K); [iSolveTC|..])
       |fail 1 "wp_store: cannot find 'Store' in" e];
-    [apply _
+    [iSolveTC
     |solve_mapsto ()
     |env_cbv; reflexivity
     |finish ()]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_store _ _ _ _ _ K); [apply _|..])
+         eapply (tac_twp_store _ _ _ _ _ K); [iSolveTC|..])
       |fail 1 "wp_store: cannot find 'Store' in" e];
     [solve_mapsto ()
     |env_cbv; reflexivity
@@ -400,16 +400,16 @@ Tactic Notation "wp_cas_fail" :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..])
+         eapply (tac_wp_cas_fail _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
-    [apply _
+    [iSolveTC
     |solve_mapsto ()
     |try congruence
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_cas_fail _ _ _ _ K); [apply _|apply _|..])
+         eapply (tac_twp_cas_fail _ _ _ _ K); [iSolveTC|iSolveTC|..])
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
@@ -426,9 +426,9 @@ Tactic Notation "wp_cas_suc" :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [apply _|apply _|..])
+         eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
-    [apply _
+    [iSolveTC
     |solve_mapsto ()
     |try congruence
     |env_cbv; reflexivity
@@ -436,7 +436,7 @@ Tactic Notation "wp_cas_suc" :=
   | |- envs_entails _ (twp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
+         eapply (tac_twp_cas_suc _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
@@ -454,16 +454,16 @@ Tactic Notation "wp_faa" :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_faa _ _ _ _ _ _ K); [apply _|..])
+         eapply (tac_wp_faa _ _ _ _ _ _ K); [iSolveTC|..])
       |fail 1 "wp_faa: cannot find 'CAS' in" e];
-    [apply _
+    [iSolveTC
     |solve_mapsto ()
     |env_cbv; reflexivity
     |wp_expr_simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_faa _ _ _ _ _ K); [apply _|..])
+         eapply (tac_twp_faa _ _ _ _ _ K); [iSolveTC|..])
       |fail 1 "wp_faa: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |env_cbv; reflexivity
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 3874e71e4aa6ed5e1195b43a3bac1b84491e0a27..e48d17176c9275f4be9cf15a9a5a15ae1d72f1b5 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -66,7 +66,7 @@ Tactic Notation "iStartProof" :=
   lazymatch goal with
   | |- envs_entails _ _ => idtac
   | |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
-               [apply _ || fail "iStartProof: not a Bi entailment"
+               [iSolveTC || fail "iStartProof: not a Bi entailment"
                |apply tac_adequate]
   end.
 
@@ -87,7 +87,7 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
      [bi_car _], and hence trigger the canonical structures mechanism
      to find the corresponding bi. *)
   | |- ?φ => notypeclasses refine ((λ P : PROP, @as_emp_valid_2 φ _ P) _ _ _);
-               [apply _ || fail "iStartProof: not a Bi entailment"
+               [iSolveTC || fail "iStartProof: not a Bi entailment"
                |apply tac_adequate]
   end.
 
@@ -171,7 +171,7 @@ Ltac iElaborateSelPat pat :=
 Local Ltac iClearHyp H :=
   eapply tac_clear with _ H _ _; (* (i:=H) *)
     [env_reflexivity || fail "iClear:" H "not found"
-    |env_cbv; apply _ ||
+    |env_cbv; iSolveTC ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail "iClear:" H ":" P "not affine and the goal not absorbing"
     |].
@@ -192,10 +192,10 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
 Tactic Notation "iExact" constr(H) :=
   eapply tac_assumption with _ H _ _; (* (i:=H) *)
     [env_reflexivity || fail "iExact:" H "not found"
-    |apply _ ||
+    |iSolveTC ||
      let P := match goal with |- FromAssumption _ ?P _ => P end in
      fail "iExact:" H ":" P "does not match goal"
-    |env_cbv; apply _ ||
+    |env_cbv; iSolveTC ||
      fail "iExact:" H "not absorbing and the remaining hypotheses not affine"].
 
 Tactic Notation "iAssumptionCore" :=
@@ -223,7 +223,7 @@ Tactic Notation "iAssumption" :=
         eapply (tac_assumption _ _ j p P);
           [env_reflexivity
           |apply Hass
-          |env_cbv; apply _ ||
+          |env_cbv; iSolveTC ||
            fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"]
        |assert (P = False%I) as Hass by reflexivity;
         apply (tac_false_destruct _ j p P);
@@ -244,10 +244,10 @@ Tactic Notation "iExFalso" := apply tac_ex_falso.
 Local Tactic Notation "iPersistent" constr(H) :=
   eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
     [env_reflexivity || fail "iPersistent:" H "not found"
-    |apply _ ||
+    |iSolveTC ||
      let P := match goal with |- IntoPersistent _ ?P _ => P end in
      fail "iPersistent:" P "not persistent"
-    |env_cbv; apply _ ||
+    |env_cbv; iSolveTC ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail "iPersistent:" P "not affine and the goal not absorbing"
     |env_reflexivity|].
@@ -255,10 +255,10 @@ Local Tactic Notation "iPersistent" constr(H) :=
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
     [env_reflexivity || fail "iPure:" H "not found"
-    |apply _ ||
+    |iSolveTC ||
      let P := match goal with |- IntoPure ?P _ => P end in
      fail "iPure:" P "not pure"
-    |env_cbv; apply _ ||
+    |env_cbv; iSolveTC ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail "iPure:" P "not affine and the goal not absorbing"
     |intros pat].
@@ -266,14 +266,14 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
 Tactic Notation "iEmpIntro" :=
   iStartProof;
   eapply tac_emp_intro;
-    [env_cbv; apply _ ||
+    [env_cbv; iSolveTC ||
      fail "iEmpIntro: spatial context contains non-affine hypotheses"].
 
 Tactic Notation "iPureIntro" :=
   iStartProof;
   eapply tac_pure_intro;
     [env_reflexivity
-    |apply _ ||
+    |iSolveTC ||
      let P := match goal with |- FromPure _ ?P _ => P end in
      fail "iPureIntro:" P "not pure"
     |].
@@ -290,14 +290,14 @@ Local Ltac iFramePure t :=
   iStartProof;
   let φ := type of t in
   eapply (tac_frame_pure _ _ _ _ t);
-    [apply _ || fail "iFrame: cannot frame" φ
+    [iSolveTC || fail "iFrame: cannot frame" φ
     |iFrameFinish].
 
 Local Ltac iFrameHyp H :=
   iStartProof;
   eapply tac_frame with _ H _ _ _;
     [env_reflexivity || fail "iFrame:" H "not found"
-    |apply _ ||
+    |iSolveTC ||
      let R := match goal with |- Frame _ ?R _ _ => R end in
      fail "iFrame: cannot frame" R
     |iFrameFinish].
@@ -389,7 +389,7 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
      lazymatch goal with
      | |- envs_entails _ _ =>
        eapply tac_forall_intro;
-       [apply _ ||
+       [iSolveTC ||
               let P := match goal with |- FromForall ?P _ => P end in
               fail "iIntro: cannot turn" P "into a universal quantifier"
        |lazy beta; intros x]
@@ -400,17 +400,17 @@ Local Tactic Notation "iIntro" constr(H) :=
   first
   [ (* (?Q → _) *)
     eapply tac_impl_intro with _ H _ _ _; (* (i:=H) *)
-      [apply _
-      |env_cbv; apply _ ||
+      [iSolveTC
+      |env_cbv; iSolveTC ||
        let P := lazymatch goal with |- Persistent ?P => P end in
        fail 1 "iIntro: introducing non-persistent" H ":" P
               "into non-empty spatial context"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
-      |apply _
+      |iSolveTC
       |]
   | (* (_ -∗ _) *)
     eapply tac_wand_intro with _ H _ _; (* (i:=H) *)
-      [apply _
+      [iSolveTC
       | env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
   | fail "iIntro: nothing to introduce" ].
@@ -420,19 +420,19 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
   first
   [ (* (?P → _) *)
     eapply tac_impl_intro_persistent with _ H _ _ _; (* (i:=H) *)
-      [apply _
-      |apply _ ||
+      [iSolveTC
+      |iSolveTC ||
        let P := match goal with |- IntoPersistent _ ?P _ => P end in
        fail 1 "iIntro:" P "not persistent"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
   | (* (?P -∗ _) *)
     eapply tac_wand_intro_persistent with _ H _ _ _; (* (i:=H) *)
-      [ apply _
-      | apply _ ||
+      [ iSolveTC
+      | iSolveTC ||
        let P := match goal with |- IntoPersistent _ ?P _ => P end in
        fail 1 "iIntro:" P "not persistent"
-      |apply _ ||
+      |iSolveTC ||
        let P := match goal with |- TCOr (Affine ?P) _ => P end in
        fail 1 "iIntro:" P "not affine and the goal not absorbing"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
@@ -443,11 +443,11 @@ Local Tactic Notation "iIntro" "_" :=
   first
   [ (* (?Q → _) *)
     iStartProof; eapply tac_impl_intro_drop;
-    [ apply _ | ]
+    [ iSolveTC | ]
   | (* (_ -∗ _) *)
     iStartProof; eapply tac_wand_intro_drop;
-      [ apply _
-      | apply _ ||
+      [ iSolveTC
+      | iSolveTC ||
        let P := match goal with |- TCOr (Affine ?P) _ => P end in
        fail 1 "iIntro:" P "not affine and the goal not absorbing"
       |]