diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 3439ddebef9b3bbc52b10827fe6f26cd527cba43..2c3237806f9650fcc5bf6100529eea27380ff524 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1078,10 +1078,17 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
     end
   end.
 
+(** To finish the user-facing [iSpecialize] tactics we call [resolve_tc] to
+solve remaining TC obligations in the given term [t]. See [test_iSpecialize_tc]
+for a test.
+
+Note that we do not call [resolve_tc] in the internal [iSpecializeCore] tactics
+above, because that would be too eager. It will only be called in the very end
+by [iPoseProofCore] below. *)
 Tactic Notation "iSpecialize" open_constr(t) :=
-  iSpecializeCore t as false.
+  iSpecializeCore t as false; resolve_tc t.
 Tactic Notation "iSpecialize" open_constr(t) "as" "#" :=
-  iSpecializeCore t as true.
+  iSpecializeCore t as true; resolve_tc t.
 
 (** The tactic [iPoseProofCore lem as p tac] inserts the resource
 described by [lem] into the context. The tactic takes a continuation [tac] as
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 4d6ba28dbc18214925781da990ee7655feece151..a2c768b7d4dbd87dc239bf05249b0589fda5ba1b 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -636,9 +636,7 @@ Proof. iExists {[ 1%positive ]}, ∅. auto. Qed.
 
 Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P.
 Proof.
-  iIntros "H".
-  (* FIXME: this [unshelve] and [apply _] should not be needed. *)
-  unshelve iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅); try apply _. done.
+  iIntros "H". iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅). done.
 Qed.
 
 Lemma test_iFrame_pure `{!BiInternalEq PROP} {A : ofe} (φ : Prop) (y z : A) :