diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 5bba0af79ae147b05f0eb98847b270cb5124cf37..7f6cca12d92a8949c6cbbb2bb8f454022cd56b02 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -225,14 +225,14 @@ Qed.
 
 Tactic Notation "tp_xchg" constr(j) :=
   iStartProof;
-  eapply (tac_tp_store j);
-  [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"
+  eapply (tac_tp_xchg j);
+  [tc_solve || fail "tp_xchg: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_xchg: cannot prove 'nclose specN ⊆ ?'"
+  |iAssumptionCore || fail "tp_xchg: cannot find '" j " ' RHS"
   |tp_bind_helper
-  |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"
+  |tc_solve || fail "tp_xchg: cannot convert the argument to a value"
+  |iAssumptionCore || fail "tp_xchg: cannot find '? ↦ₛ ?'"
+  |simpl; reflexivity || fail "tp_xchg: this should not happen"
   |pm_reduce (* new goal *)].
 
 (* *)
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 2d32037c6785948a0041bfc0410ce301fdb91d3f..374ecd84f48e98f20609b679d3818b3119ed849d 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -195,9 +195,9 @@ Section rules.
     rewrite /IntoVal. iIntros (?<-) "Hl Hlog".
     iApply refines_step_r.
     iIntros (k) "Hk".
-    admit.
-  Admitted.
-
+    tp_xchg k. iExists v. iModIntro. iFrame.
+    by iApply "Hlog".
+  Qed.
 
   Lemma refines_cmpxchg_fail_r E K l e1 e2 v1 v2 v t A :
     nclose specN ⊆ E →