diff --git a/semantics.opam b/semantics.opam
index 28595fcfc687e2d211363946b62d83975450167f..6324efb19135e2c8a8787acb1a9c16c7dc9837c2 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -10,7 +10,7 @@ version: "dev"
 
 depends: [
   "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2022-09-29.0.b335afaf") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-11-24.2.5b5d3f4d") | (= "dev") }
   "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15")  | (= "1.3+8.16") }
   "coq-autosubst" { (= "1.7") | (= "dev")  }
 ]
diff --git a/theories/program_logics/heap_lang/proofmode.v b/theories/program_logics/heap_lang/proofmode.v
index 77631c1c92dacfb831a28f9b99aadc3c98b57879..46da3d41187bdc55b95f45da026e1e112d1ec4a9 100644
--- a/theories/program_logics/heap_lang/proofmode.v
+++ b/theories/program_logics/heap_lang/proofmode.v
@@ -75,10 +75,10 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     reshape_expr e ltac:(fun K e' =>
       unify e' efoc;
       eapply (tac_wp_pure _ _ _ _ _ K e');
-      [iSolveTC                       (* PureExec *)
+      [tc_solve                       (* PureExec *)
       |try solve_vals_compare_safe    (* The pure condition for PureExec --
          handles trivial goals, including [vals_compare_safe] *)
-      |iSolveTC                       (* IntoLaters *)
+      |tc_solve                       (* IntoLaters *)
       |wp_finish                      (* new goal *)
       ])
     || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
@@ -322,14 +322,14 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
         first
           [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ _ Htmp K))
           |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
-        [iSolveTC
+        [tc_solve
         |finish ()]
     in
     let process_array _ :=
         first
           [reshape_expr e ltac:(fun K e' => eapply (tac_wp_allocN _ _ _ _ _ Htmp K))
           |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
-        [idtac|iSolveTC
+        [idtac|tc_solve
          |finish ()]
     in (process_single ()) || (process_array ())
   | _ => fail "wp_alloc: not a 'wp'"
@@ -348,7 +348,7 @@ Tactic Notation "wp_free" :=
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_free _ _ _ _ _ _ K))
       |fail 1 "wp_free: cannot find 'Free' in" e];
-    [iSolveTC
+    [tc_solve
     |solve_mapsto ()
     |pm_reduce; wp_finish]
   | _ => fail "wp_free: not a 'wp'"
@@ -364,7 +364,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];
-    [iSolveTC
+    [tc_solve
     |solve_mapsto ()
     |wp_finish]
   | _ => fail "wp_load: not a 'wp'"
@@ -380,7 +380,7 @@ Tactic Notation "wp_store" :=
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ _ K))
       |fail 1 "wp_store: cannot find 'Store' in" e];
-    [iSolveTC
+    [tc_solve
     |solve_mapsto ()
     |pm_reduce; first [wp_seq|wp_finish]]
   | _ => fail "wp_store: not a 'wp'"
diff --git a/theories/program_logics/reloc/proofmode.v b/theories/program_logics/reloc/proofmode.v
index 2bfc11f4cdcf28b228adc276238d8076c6fb6511..f9e051d364b8d7f3c3661f7eca1540b88f80b0b2 100644
--- a/theories/program_logics/reloc/proofmode.v
+++ b/theories/program_logics/reloc/proofmode.v
@@ -113,9 +113,9 @@ Tactic Notation "src_pure" open_constr(ef) :=
     reshape_expr e ltac:(fun K e' =>
       unify e' ef;
       eapply (tac_src_pure (fill K' e) (K++K') e');
-      [by rewrite ?fill_app | iSolveTC | ..])
+      [by rewrite ?fill_app | tc_solve | ..])
   end;
-  [iSolveTC || fail "src_pure: cannot eliminate modality in the goal"
+  [tc_solve || fail "src_pure: cannot eliminate modality in the goal"
   |solve_ndisj || fail "src_pure: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "src_pure: cannot find the RHS"
   |try (exact I || reflexivity) (* ψ *)
@@ -191,11 +191,11 @@ Qed.
 Tactic Notation "src_store" :=
   iStartProof;
   eapply (tac_src_store);
-  [iSolveTC || fail "src_store: cannot eliminate modality in the goal"
+  [tc_solve || fail "src_store: cannot eliminate modality in the goal"
   |solve_ndisj || fail "src_store: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "src_store: cannot find RHS"
   |src_bind_helper
-  |iSolveTC || fail "src_store: cannot convert the argument to a value"
+  |tc_solve || fail "src_store: cannot convert the argument to a value"
   |simpl; reflexivity || fail "src_store: this should not happen"
   |iAssumptionCore || fail "src_store: cannot find '? ↦ₛ ?'"
   |pm_reduce (* new goal *)].
@@ -243,7 +243,7 @@ Qed.
 Tactic Notation "src_load" :=
   iStartProof;
   eapply (tac_src_load);
-  [iSolveTC || fail "src_load: cannot eliminate modality in the goal"
+  [tc_solve || fail "src_load: cannot eliminate modality in the goal"
   |solve_ndisj || fail "src_load: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "src_load: cannot find the RHS"
   |src_bind_helper
@@ -298,11 +298,11 @@ Tactic Notation "src_alloc" ident(l) "as" constr(H) :=
         | (iIntros H; src_normalise) || fail 1 "src_alloc:" H "not correct intro pattern" ] in
   iStartProof;
   eapply (tac_src_alloc);
-  [iSolveTC || fail "src_alloc: cannot eliminate modality in the goal"
+  [tc_solve || fail "src_alloc: cannot eliminate modality in the goal"
   |solve_ndisj || fail "src_alloc: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "src_alloc: cannot find the RHS"
   |src_bind_helper
-  |iSolveTC || fail "src_alloc: expressions is not a value"
+  |tc_solve || fail "src_alloc: expressions is not a value"
   |finish ()
 (* new goal *)].