diff --git a/coq-reloc.opam b/coq-reloc.opam
index a2f54de6a9c820260ea88f9a98a0af91a0bc3e82..656929ad3b524f74798bdd32477059444d717513 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2022-08-12.4.9245c4c0") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-11-29.1.c44ce4c9") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 0e7b615f03a56a679608eb6b39f2a11f3d89224f..5bba0af79ae147b05f0eb98847b270cb5124cf37 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -104,14 +104,14 @@ Tactic Notation "tp_pure" constr(j) open_constr(ef) :=
     reshape_expr e ltac:(fun K e' =>
       unify e' ef;
       eapply (tac_tp_pure (fill K' e) (K++K') e' j);
-      [by rewrite ?fill_app | iSolveTC | ..])
+      [by rewrite ?fill_app | tc_solve | ..])
   | |- context[environments.Esnoc _ ?H (refines_right j ?e)] =>
     reshape_expr e ltac:(fun K e' =>
       unify e' ef;
       eapply (tac_tp_pure e K e' j);
-      [by rewrite ?fill_app | iSolveTC | ..])
+      [by rewrite ?fill_app | tc_solve | ..])
   end;
-  [iSolveTC || fail "tp_pure: cannot eliminate modality in the goal"
+  [tc_solve || fail "tp_pure: cannot eliminate modality in the goal"
   |solve_ndisj || fail "tp_pure: cannot prove 'nclose specN ⊆ ?'"
   (* |iAssumptionCore || fail "tp_pure: cannot find spec_ctx" (* spec_ctx *) *)
   |iAssumptionCore || fail "tp_pure: cannot find the RHS" (* TODO fix error message *)
@@ -181,11 +181,11 @@ Qed.
 Tactic Notation "tp_store" constr(j) :=
   iStartProof;
   eapply (tac_tp_store j);
-  [iSolveTC || fail "tp_store: cannot eliminate modality in the goal"
+  [tc_solve || fail "tp_store: cannot eliminate modality in the goal"
   |solve_ndisj || fail "tp_store: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "tp_store: cannot find '" j " ' RHS"
   |tp_bind_helper
-  |iSolveTC || fail "tp_store: cannot convert the argument to a value"
+  |tc_solve || fail "tp_store: cannot convert the argument to a value"
   |simpl; reflexivity || fail "tp_store: this should not happen"
   |iAssumptionCore || fail "tp_store: cannot find '? ↦ₛ ?'"
   |pm_reduce (* new goal *)].
@@ -226,11 +226,11 @@ Qed.
 Tactic Notation "tp_xchg" constr(j) :=
   iStartProof;
   eapply (tac_tp_store j);
-  [iSolveTC || fail "tp_store: cannot eliminate modality in the goal"
+  [tc_solve || fail "tp_store: cannot eliminate modality in the goal"
   |solve_ndisj || fail "tp_store: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "tp_store: cannot find '" j " ' RHS"
   |tp_bind_helper
-  |iSolveTC || fail "tp_store: cannot convert the argument to a value"
+  |tc_solve || fail "tp_store: cannot convert the argument to a value"
   |iAssumptionCore || fail "tp_store: cannot find '? ↦ₛ ?'"
   |simpl; reflexivity || fail "tp_store: this should not happen"
   |pm_reduce (* new goal *)].
@@ -278,7 +278,7 @@ Qed.
 Tactic Notation "tp_load" constr(j) :=
   iStartProof;
   eapply (tac_tp_load j);
-  [iSolveTC || fail "tp_load: cannot eliminate modality in the goal"
+  [tc_solve || fail "tp_load: cannot eliminate modality in the goal"
   |solve_ndisj || fail "tp_load: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "tp_load: cannot find the RHS '" j "'"
   |tp_bind_helper
@@ -325,12 +325,12 @@ Qed.
 Tactic Notation "tp_cmpxchg_fail" constr(j) :=
   iStartProof;
   eapply (tac_tp_cmpxchg_fail j);
-    [iSolveTC || fail "tp_cmpxchg_fail: cannot eliminate modality in the goal"
+    [tc_solve || fail "tp_cmpxchg_fail: cannot eliminate modality in the goal"
     |solve_ndisj || fail "tp_cmpxchg_fail: cannot prove 'nclose specN ⊆ ?'"
     |iAssumptionCore || fail "tp_cmpxchg_fail: cannot find the RHS '" j "'"
     |tp_bind_helper (* e = K'[CmpXchg _ _ _] *)
-    |iSolveTC || fail "tp_cmpxchg_fail: argument is not a value"
-    |iSolveTC || fail "tp_cmpxchg_fail: argument is not a value"
+    |tc_solve || fail "tp_cmpxchg_fail: argument is not a value"
+    |tc_solve || fail "tp_cmpxchg_fail: argument is not a value"
     |iAssumptionCore || fail "tp_cmpxchg_fail: cannot find '? ↦ ?'"
     |try (simpl; congruence) (* v' ≠ v1 *)
     |try heap_lang.proofmode.solve_vals_compare_safe
@@ -374,12 +374,12 @@ Qed.
 Tactic Notation "tp_cmpxchg_suc" constr(j) :=
   iStartProof;
   eapply (tac_tp_cmpxchg_suc j);
-  [iSolveTC || fail "tp_cmpxchg_suc: cannot eliminate modality in the goal"
+  [tc_solve || fail "tp_cmpxchg_suc: cannot eliminate modality in the goal"
   |solve_ndisj || fail "tp_cmpxchg_suc: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "tp_cmpxchg_suc: cannot the RHS '" j "'"
   |tp_bind_helper (* e = K'[CmpXchg _ _ _] *)
-  |iSolveTC || fail "tp_cmpxchg_suc: argument is not a value"
-  |iSolveTC || fail "tp_cmpxchg_suc: argument is not a value"
+  |tc_solve || fail "tp_cmpxchg_suc: argument is not a value"
+  |tc_solve || fail "tp_cmpxchg_suc: argument is not a value"
   |iAssumptionCore || fail "tp_cmpxchg_suc: cannot find '? ↦ ?'"
   |try (simpl; congruence)     (* v' = v1 *)
   |try heap_lang.proofmode.solve_vals_compare_safe
@@ -420,11 +420,11 @@ Qed.
 Tactic Notation "tp_faa" constr(j) :=
   iStartProof;
   eapply (tac_tp_faa j);
-  [iSolveTC || fail "tp_faa: cannot eliminate modality in the goal"
+  [tc_solve || fail "tp_faa: cannot eliminate modality in the goal"
   |solve_ndisj || fail "tp_faa: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "tp_faa: cannot find the RHS '" j "'"
   |tp_bind_helper (* e = K'[FAA _ _ _] *)
-  |iSolveTC (* IntoVal *)
+  |tc_solve (* IntoVal *)
   |iAssumptionCore || fail "tp_faa: cannot find '? ↦ ?'"
   |simpl;reflexivity || fail "tp_faa: this should not happen"
   |pm_reduce (* new goal *)].
@@ -466,7 +466,7 @@ Qed.
 Tactic Notation "tp_fork" constr(j) :=
   iStartProof;
   eapply (tac_tp_fork j);
-  [iSolveTC || fail "tp_fork: cannot eliminate modality in the goal"
+  [tc_solve || fail "tp_fork: cannot eliminate modality in the goal"
   |solve_ndisj || fail "tp_fork: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "tp_fork: cannot find the RHS '" j "'"
   |tp_bind_helper
@@ -476,7 +476,7 @@ Tactic Notation "tp_fork" constr(j) :=
 Tactic Notation "tp_fork" constr(j) "as" ident(j') constr(H) :=
   iStartProof;
   eapply (tac_tp_fork j);
-  [iSolveTC || fail "tp_fork: cannot eliminate modality in the goal"
+  [tc_solve || fail "tp_fork: cannot eliminate modality in the goal"
   |solve_ndisj || fail "tp_fork: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "tp_fork: cannot find the RHS '" j "'"
   |tp_bind_helper
@@ -531,11 +531,11 @@ Tactic Notation "tp_alloc" constr(j) "as" ident(l) constr(H) :=
         | (iIntros H; tp_normalise j) || fail 1 "tp_alloc:" H "not correct intro pattern" ] in
   iStartProof;
   eapply (tac_tp_alloc j);
-  [iSolveTC || fail "tp_alloc: cannot eliminate modality in the goal"
+  [tc_solve || fail "tp_alloc: cannot eliminate modality in the goal"
   |solve_ndisj || fail "tp_alloc: cannot prove 'nclose specN ⊆ ?'"
   |iAssumptionCore || fail "tp_alloc: cannot find the RHS '" j "'"
   |tp_bind_helper
-  |iSolveTC || fail "tp_alloc: expressions is not a value"
+  |tc_solve || fail "tp_alloc: expressions is not a value"
   |finish ()
 (* new goal *)].
 
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index e61fe68add0072427519b95d24effd0c3e401039..de6e53fbd8ae1e0fa4c6c1d1935a930f5afe1767 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -160,12 +160,12 @@ Tactic Notation "rel_pure_l" open_constr(ef) :=
       unify e' ef;
       eapply (tac_rel_pure_l K e');
       [reflexivity                  (** e = fill K e' *)
-      |iSolveTC                     (** PureClosed Ï• e' e2 *)
+      |tc_solve                     (** PureClosed Ï• e' e2 *)
       | .. ]);
       [try heap_lang.proofmode.solve_vals_compare_safe                (** φ *)
       |first [left; split; reflexivity              (** Here we decide if the mask E is ⊤ *)
              | right; reflexivity]                  (**    (m = n ∧ E = ⊤) ∨ (m = 0) *)
-      |iSolveTC                                     (** IntoLaters *)
+      |tc_solve                                     (** IntoLaters *)
       |simpl; reflexivity           (** eres = fill K e2 *)
       |rel_finish                   (** new goal *)]
   || fail "rel_pure_l: cannot find the reduct".
@@ -178,7 +178,7 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
       unify e' ef;
       eapply (tac_rel_pure_r K e');
       [reflexivity                  (** e = fill K e1 *)
-      |iSolveTC                     (** PureClosed Ï• e1 e2 *)
+      |tc_solve                     (** PureClosed Ï• e1 e2 *)
       |..]);
       [try heap_lang.proofmode.solve_vals_compare_safe                (** φ *)
       |solve_ndisj        || fail 1 "rel_pure_r: cannot solve ↑specN ⊆ ?"
@@ -242,7 +242,7 @@ Tactic Notation "rel_load_l" :=
        eapply (tac_rel_load_l_simp K); first reflexivity)
     |fail 1 "rel_load_l: cannot find 'Load'"];
   (* the remaining goals are from tac_lel_load_l (except for the first one, which has already been solved by this point) *)
-  [iSolveTC             (** IntoLaters *)
+  [tc_solve             (** IntoLaters *)
   |solve_mapsto ()
   |reflexivity       (** eres = fill K v *)
   |rel_finish  (** new goal *)].
@@ -319,11 +319,11 @@ Tactic Notation "rel_store_l" :=
     [rel_reshape_cont_l ltac:(fun K e' =>
        eapply (tac_rel_store_l_simpl K);
        [reflexivity (** e = fill K (#l <- e') *)
-       |iSolveTC    (** e' is a value *)
+       |tc_solve    (** e' is a value *)
        |idtac..])
     |fail 1 "rel_store_l: cannot find 'Store'"];
   (* the remaining goals are from tac_rel_store_l (except for the first one, which has already been solved by this point) *)
-  [iSolveTC        (** IntoLaters *)
+  [tc_solve        (** IntoLaters *)
   |solve_mapsto ()
   |pm_reflexivity || fail "rel_store_l: this should not happen O-:"
   |reflexivity
@@ -339,7 +339,7 @@ Tactic Notation "rel_store_r" :=
   first
     [rel_reshape_cont_r ltac:(fun K e' =>
        eapply (tac_rel_store_r K);
-       [reflexivity|iSolveTC|idtac..])
+       [reflexivity|tc_solve|idtac..])
     |fail 1 "rel_store_r: cannot find 'Store'"];
   (* the remaining goals are from tac_rel_store_r (except for the first one, which has already been solved by this point) *)
   [solve_ndisj || fail "rel_store_r: cannot prove 'nclose specN ⊆ ?'"
@@ -398,11 +398,11 @@ Tactic Notation "rel_xchg_l" :=
     [rel_reshape_cont_l ltac:(fun K e' =>
        eapply (tac_rel_xchg_l_simpl K);
        [reflexivity (** e = fill K (#l <- e') *)
-       |iSolveTC    (** e' is a value *)
+       |tc_solve    (** e' is a value *)
        |idtac..])
     |fail 1 "rel_xchg_l: cannot find 'Xchg'"];
   (* the remaining goals are from tac_rel_xchg_l (except for the first one, which has already been solved by this point) *)
-  [iSolveTC        (** IntoLaters *)
+  [tc_solve        (** IntoLaters *)
   |solve_mapsto ()
   |pm_reflexivity || fail "rel_xchg_l: this should not happen O-:"
   |reflexivity
@@ -418,7 +418,7 @@ Tactic Notation "rel_xchg_r" :=
   first
     [rel_reshape_cont_r ltac:(fun K e' =>
        eapply (tac_rel_xchg_r K);
-       [reflexivity|iSolveTC|idtac..])
+       [reflexivity|tc_solve|idtac..])
     |fail 1 "rel_xchg_r: cannot find 'Xchg'"];
   (* the remaining goals are from tac_rel_xchg_r (except for the first one, which has already been solved by this point) *)
   [solve_ndisj || fail "rel_xchg_r: cannot prove 'nclose specN ⊆ ?'"
@@ -452,10 +452,10 @@ Tactic Notation "rel_alloc_l" ident(l) "as" constr(H) :=
     [rel_reshape_cont_l ltac:(fun K e' =>
        eapply (tac_rel_alloc_l_simpl K);
        [reflexivity (** e = fill K (Alloc e') *)
-       |iSolveTC    (** e' is a value *)
+       |tc_solve    (** e' is a value *)
        |idtac..])
     |fail 1 "rel_alloc_l: cannot find 'Alloc'"];
-  [iSolveTC        (** IntoLaters *)
+  [tc_solve        (** IntoLaters *)
   |iIntros (l) H; rel_finish  (** new goal *)].
 
 Lemma tac_rel_alloc_r `{!relocG Σ} K' ℶ E t' v' e t A :
@@ -475,7 +475,7 @@ Tactic Notation "rel_alloc_r" ident(l) "as" constr(H) :=
     [rel_reshape_cont_r ltac:(fun K e' =>
        eapply (tac_rel_alloc_r K);
        [reflexivity  (** t = K'[alloc t'] *)
-       |iSolveTC     (** t' is a value *)
+       |tc_solve     (** t' is a value *)
        |idtac..])
     |fail 1 "rel_alloc_r: cannot find 'Alloc'"];
   [solve_ndisj || fail "rel_alloc_r: cannot prove 'nclose specN ⊆ ?'"
@@ -544,8 +544,8 @@ Tactic Notation "rel_cmpxchg_fail_r" :=
     [rel_reshape_cont_r ltac:(fun K e' =>
        eapply (tac_rel_cmpxchg_fail_r K);
        [reflexivity  (** e = fill K (CmpXchg #l e1 e2) *)
-       |iSolveTC     (** e1 is a value *)
-       |iSolveTC     (** e2 is a value *)
+       |tc_solve     (** e1 is a value *)
+       |tc_solve     (** e2 is a value *)
        |idtac..])
     |fail 1 "rel_cmpxchg_fail_r: cannot find 'CmpXchg'"];
   (* the remaining goals are from tac_rel_cmpxchg_fail_r (except for the first one, which has already been solved by this point) *)
@@ -565,8 +565,8 @@ Tactic Notation "rel_cmpxchg_suc_r" :=
     [rel_reshape_cont_r ltac:(fun K e' =>
        eapply (tac_rel_cmpxchg_suc_r K);
        [reflexivity  (** e = fill K (CmpXchg #l e1 e2) *)
-       |iSolveTC     (** e1 is a value *)
-       |iSolveTC     (** e2 is a value *)
+       |tc_solve     (** e1 is a value *)
+       |tc_solve     (** e2 is a value *)
        |idtac..])
     |fail 1 "rel_cmpxchg_suc_r: cannot find 'CmpXchg'"];
   (* the remaining goals are from tac_rel_cmpxchg_suc_r (except for the first one, which has already been solved by this point) *)
@@ -603,7 +603,7 @@ Tactic Notation "rel_newproph_l" ident(p) ident(vs) "as" constr(H) :=
        [reflexivity (** e = fill K (NewProph e') *)
        |idtac..])
     |fail 1 "rel_newproph_l: cannot find 'NewProph'"];
-  [iSolveTC                      (** IntoLaters *)
+  [tc_solve                      (** IntoLaters *)
   |iIntros (p vs) H; rel_finish  (** new goal *)].
 
 Lemma tac_rel_newproph_r `{!relocG Σ} K' ℶ E e t A :