diff --git a/theories/examples/par.v b/theories/examples/par.v
index da0301516055a637ced01aae0207c77a79b02e57..62a7e012b23e47f35d4b6008d99ac843edd7fb27 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -33,10 +33,9 @@ Section rules.
     repeat rel_pure_r. rel_fork_r i as "Hi".
     { simpl. eauto. }
     repeat rel_pure_r.
-    tp_rec i. simpl.
-    tp_bind i e1.
+    tp_pure i _. tp_bind i e1.
     iMod ("H" with "Hi") as (v1) "[Hi H]".
-    iSimpl in "Hi". tp_pure i (InjR v1). tp_store i.
+    iSimpl in "Hi". tp_pure i _. tp_store i.
   Abort.
     (* rewrite refines_eq /refines_def. *)
     (* iIntros (ρ') "_". clear ρ'. *)
@@ -77,7 +76,7 @@ Section rules.
     repeat rel_pure_r. rel_fork_r i as "Hi".
     repeat rel_pure_r.
     tp_rec i. simpl.
-    tp_pure i (InjR _). tp_store i.
+    tp_pure i _. tp_store i.
     rel_bind_l e. rel_bind_r e.
     iApply (refines_bind with "H").
     iIntros (v v') "Hv". simpl.
@@ -123,17 +122,11 @@ Section rules.
       iApply (join_spec with "l_hndl").
       iNext. iIntros (w1). iDestruct 1 as (w2) "[Hj Hw]".
       unfold C. iSimpl in "Hi". iSimpl in "Hj".
-      tp_pure i (InjR v2). iSimpl in "Hi".
-      tp_store i.
-      (* TODO: better tp_pure tactics *)
-      tp_pure j (Lam _ _). simpl.
-      tp_rec j. simpl.
-      tp_bind j (spawn.join _). unlock spawn.join.
-      tp_pure j (App _ #c2). simpl.
-      iApply fupd_wp. tp_load j. simpl.
-      tp_pure j (Case _ _ _). tp_pure j (Lam _ _). simpl.
-      tp_pure j (App _ v2). simpl. tp_pure j (Lam _ _). simpl.
-      tp_pure j _. simpl. tp_pure j _.
+      tp_pures i. tp_store i.
+      tp_pures j.
+      tp_rec j.
+      tp_pures j. iApply fupd_wp. tp_load j. tp_normalise j.
+      tp_pures j.
       iModIntro. wp_pures. iExists (v2, w2)%V. eauto.
   Qed.
 
@@ -167,17 +160,11 @@ Section rules.
     iApply (wp_wand with "He2"). iIntros (w1).
     iDestruct 1 as (w2) "[Hj Hw]".
     iSimpl in "Hi". iSimpl in "Hj".
-    tp_pure i (InjR v2). iSimpl in "Hi".
+    tp_pure i _. iSimpl in "Hi".
     tp_store i.
-    (* TODO: better tp_pure tactics *)
-    tp_pure j (Lam _ _). simpl.
-    tp_rec j. simpl.
-    tp_bind j (spawn.join _). unlock spawn.join.
-    tp_pure j (App _ #c2). simpl.
-    tp_load j. simpl.
-    tp_pure j (Case _ _ _). tp_pure j (Lam _ _). simpl.
-    tp_pure j (App _ v2). simpl. tp_pure j (Lam _ _). simpl.
-    tp_pure j _. simpl. tp_pure j _.
+    tp_pures j. tp_rec j.
+    tp_load j. tp_normalise j.
+    tp_pures j.
     iModIntro. iExists _. iFrame.
   Qed.
 
@@ -219,12 +206,7 @@ Section rules.
       wp_pures. wp_bind (spawn.join _).
       iApply (join_spec with "Hdl").
       iNext. iIntros (av). iDestruct 1 as (av') "[Hj HA]".
-      wp_pures.
-      (* TODO why is this so annoying *)
-      tp_pure j (Lam _ _). iSimpl in "Hj".
-      tp_pure j (App _ av'). iSimpl in "Hj".
-      tp_pure i (Lam _ _). iSimpl in "Hi".
-      tp_pure i (App _ bv'). iSimpl in "Hi".
+      wp_pures. tp_pures j. tp_pures i.
       wp_rec. wp_pures.
       wp_apply (spawn_spec N with "[Hc Hi]").
       { wp_pures.
@@ -242,12 +224,9 @@ Section rules.
       iIntros (cv). iDestruct 1 as (cv') "[Hi HC]".
       iApply wp_fupd.
       wp_pures. iExists (cv', dv')%V. simpl.
-      tp_pure i (InjR _). tp_store i.
-      tp_pure j (Lam _ _). tp_pure j _. simpl.
-      rewrite /spawn.join. tp_pure j (App _ #c2). simpl.
-      tp_load j. tp_case j. simpl.
-      tp_pure j (Lam _ _). tp_pure j (App _ cv'). simpl.
-      tp_pure j (Lam _ _). tp_pure j (App _ cv'). simpl.
-      tp_pure j (Pair _ _). eauto with iFrame.
+      tp_pures i. tp_store i.
+      tp_pures j.
+      rewrite /spawn.join. tp_pures j.
+      tp_load j. iSimpl in "Hj". tp_pures j. eauto with iFrame.
   Qed.
 End rules.
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index 733de55222e28080ec30cd606d911fba428a23e4..f473346a6ab6b8d9cf94e4850f1d0db7c6bfdd47 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -27,14 +27,14 @@ From reloc Require Import examples.stack.CG_stack lib.list.
 
 (** * Source code *)
 Definition pop_st_no_offer : val := λ: "r" "mb" "pop",
-  (match: !"r" with
-       NONE => NONE
-     | SOME "l" =>
-       let: "pair" := !"l" in
-       if: CAS "r" (SOME "l") (Snd "pair")
-       then SOME (Fst "pair")
-       else "pop" "r" "mb"
-     end).
+  match: !"r" with
+      NONE => NONE
+    | SOME "l" =>
+      let: "pair" := !"l" in
+      if: CAS "r" (SOME "l") (Snd "pair")
+      then SOME (Fst "pair")
+      else "pop" "r" "mb"
+  end.
 
 Definition pop_st : val := rec: "pop" "r" "mb" :=
   match: !"mb" with
@@ -49,18 +49,18 @@ Definition pop_st : val := rec: "pop" "r" "mb" :=
     end
   end.
 
-Definition push_st : val := rec: "push" "r" "mb" "n" :=
-  let: "off" := mk_offer "n" in
+Definition push_st : val := rec: "push" "r" "mb" "x" :=
+  let: "off" := mk_offer "x" in
   "mb" <- SOME "off";;
   match: revoke_offer "off" with
     NONE => (* the offer was successfully taken *) #()
-  | SOME "n" =>
+  | SOME "x" =>
     (* nobody took the offer  *)
     let: "tail" := !"r" in
-    let: "new" := SOME (ref ("n", "tail")) in
-    if: CAS "r" "tail" "new"
+    let: "hd" := SOME (ref ("x", "tail")) in
+    if: CAS "r" "tail" "hd"
     then #()
-    else "push" "r" "mb" "n"
+    else "push" "r" "mb" "x"
   end.
 
 Definition mk_stack : val :=  λ: <>,
@@ -453,37 +453,16 @@ Section refinement.
         iApply (pop_no_helping_refinement with "Hinv IH").
       + (* An offer was accepted *)
         iIntros "Hj Hoff". rel_pures_l.
-        unlock {3}CG_locked_push.
-        unlock {1}acquire {1}release.
-        (* THIS IS COPY PASTED :-) *)
-        tp_pure j (App _ (_,_)%V). iSimpl in "Hj".
-        tp_pure j (Rec _ _ _). iSimpl in "Hj".
-        repeat (tp_pure j _; iSimpl in "Hj").
-        tp_pure j (Snd _). iSimpl in "Hj".
-        unlock acquire. tp_pure j (App _ lk). iSimpl in "Hj".
+        tp_rec j. tp_pures j. tp_rec j.
         unlock is_locked_r. iDestruct "Hl" as (lk' ->) "Hl".
         (* TODO: make all the tp_ tactics work without the need for an explicit Fupd *)
         iApply refines_spec_ctx. iIntros "#Hρ".
         iApply fupd_refines.
         (* because we manually applied `fupd_refines`, the tactical `with_spec_ctx` doesn't work anymore *)
         tp_cmpxchg_suc j. iSimpl in "Hj".
-        tp_pure j (Snd _). iSimpl in "Hj".
-        tp_if j. iSimpl in "Hj".
-        tp_pure j (Rec _ _ _). iSimpl in "Hj".
-        tp_rec j. iSimpl in "Hj".
-
-        unlock CG_push.
-        tp_pure j (Fst _). iSimpl in "Hj".
-        tp_pure j (App _ #st'). iSimpl in "Hj".
-        tp_pure j (Rec _ _ _). iSimpl in "Hj".
-        tp_pure j (App _ v2). iSimpl in "Hj".
-        tp_load j. iSimpl in "Hj".
-        tp_pure j (Pair _ _).
-        tp_pure j (InjR _).
-        tp_store j. iSimpl in "Hj".
-        tp_pure j (Rec _ _ _).
-        tp_rec j. iSimpl in "Hj".
-        tp_pure j (Snd _). unlock release.
+        tp_pures j. tp_rec j. tp_pures j.
+        tp_load j. tp_normalise j. tp_pures j.
+        tp_store j. tp_normalise j. tp_pures j.
         tp_rec j. tp_store j.
         iSpecialize ("Hoff" with "Hj").
         iSpecialize ("HN" with "Hoff").
diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index d633e1c7f9d846465b46cbe1ed480fc67b635f4e..d022f7faf8ec23759d3713a1e84dea4b5bd17f48 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -64,22 +64,23 @@ Tactic Notation "tp_bind" constr(j) open_constr(efoc) :=
     |reflexivity
     |(* new goal *)].
 
-Lemma tac_tp_pure `{relocG Σ} j K' e1 e2 Δ1 Δ2 E1 i1 i2 p e ϕ ψ Q n :
+Lemma tac_tp_pure `{relocG Σ} e K' e1 j e2 Δ1 E1 i1 i2 p e' ϕ ψ Q n :
+  e = fill K' e1 →
+  PureExec ϕ n e1 e2 →
   (∀ P, ElimModal ψ false false (|={E1}=> P) P Q Q) →
   nclose specN ⊆ E1 →
   envs_lookup i1 Δ1 = Some (p, spec_ctx) →
   envs_lookup i2 Δ1 = Some (false, j ⤇ e)%I →
-  e = fill K' e1 →
-  PureExec ϕ n e1 e2 →
   ψ →
   ϕ →
-  envs_simple_replace i2 false
-    (Esnoc Enil i2
-     (j ⤇ fill K' e2)) Δ1 = Some Δ2 →
-  envs_entails Δ2 Q →
+  e' = fill K' e2 →
+  match envs_simple_replace i2 false (Esnoc Enil i2 (j ⤇ e')) Δ1 with
+  | Some Δ2 => envs_entails Δ2 Q
+  | None => False
+  end →
   envs_entails Δ1 Q.
 Proof.
-  rewrite envs_entails_eq. intros ?? HΔ1 ? Hfill Hpure Hψ Hϕ ??.
+  rewrite envs_entails_eq. intros -> Hpure ?? HΔ1 ? Hψ Hϕ -> ?.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' Δ1 false). 2: apply HΔ1.
   rewrite bi.sep_elim_l.
@@ -89,8 +90,9 @@ Proof.
     by rewrite ?(bi.intuitionistic_intuitionistically spec_ctx). }
   rewrite bi.persistently_and_intuitionistically_sep_l.
   rewrite bi.intuitionistic_intuitionistically.
+  destruct (envs_simple_replace _ _ _ _) as [Δ2|] eqn:HΔ2; try done.
   rewrite (envs_simple_replace_sound Δ1 Δ2 i2) //; simpl.
-  rewrite right_id Hfill.
+  rewrite right_id.
   rewrite (assoc _ spec_ctx (j ⤇ _)%I).
   rewrite step_pure //.
   rewrite -[Q]elim_modal // /=.
@@ -109,23 +111,37 @@ Ltac with_spec_ctx tac :=
   | _ => tac ()
   end.
 
-(* TODO: The problem here is that it will fail if the redex is not specified, and is not on the top level *)
 Tactic Notation "tp_pure" constr(j) open_constr(ef) :=
   iStartProof;
   with_spec_ctx ltac:(fun _ =>
-  eapply (tac_tp_pure j _ ef);
-    [iSolveTC || 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 '" j " ⤇ ?'"
-    |tp_bind_helper         (* e = K'[e1]*)
-    |iSolveTC               (* PureExec Ï• n e1 e2 *)
-    |try (exact I || reflexivity) (* ψ *)
-    |try (exact I || reflexivity) (* Ï• *)
-    |pm_reflexivity || fail "tp_pure: this should not happen"
-    |(* new goal *)]).
-
-Tactic Notation "tp_rec" constr(j) := tp_pure j (App _ _).
+  lazymatch goal with
+  | |- context[environments.Esnoc _ ?H (j ⤇ fill ?K' ?e)] =>
+    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 | ..])
+  | |- context[environments.Esnoc _ ?H (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 | ..])
+  end;
+  [iSolveTC || 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 '" j " ⤇ ?'"
+  |try (exact I || reflexivity) (* ψ *)
+  |try (exact I || reflexivity) (* Ï• *)
+  |simpl; reflexivity ||  fail "tp_pure: this should not happen" (* e' = fill K' e2 *)
+  |pm_reduce (* new goal *)]).
+
+
+Tactic Notation "tp_pures" constr (j) := repeat (tp_pure j _; tp_normalise j).
+Tactic Notation "tp_rec" constr(j) :=
+  let H := fresh in
+  assert (H := AsRecV_recv);
+  tp_pure j (App _ _);
+  clear H.
 Tactic Notation "tp_seq" constr(j) := tp_rec j.
 Tactic Notation "tp_let" constr(j) := tp_rec j.
 Tactic Notation "tp_lam" constr(j) := tp_rec j.
diff --git a/theories/tests/tp_tests.v b/theories/tests/tp_tests.v
index 62204210d4444361e031bc8733d5079cdae6f9a5..3dccde26bdde3f1d0fb86a0770bc84d145c2cc25 100644
--- a/theories/tests/tp_tests.v
+++ b/theories/tests/tp_tests.v
@@ -16,9 +16,7 @@ Lemma test1 E1 j K (l : loc) (n : nat) :
 Proof.
   iIntros (?) "#? Hj Hl".
   tp_load j. tp_normalise j.
-  tp_closure j. tp_normalise j.
-  tp_lam j. tp_normalise j.
-  tp_binop j. tp_normalise j.
+  tp_pures j.
   tp_store j. by iFrame.
 Qed.
 
@@ -32,11 +30,9 @@ Lemma test2 E1 j K (l : loc) (n : nat) :
 Proof.
   iIntros (?) "#? Hj Hl".
   tp_cmpxchg_fail j. tp_normalise j.
-  tp_pure j (Snd _). tp_normalise j.
-  tp_closure j. tp_normalise j.
-  tp_seq j. tp_normalise j.
-  tp_binop j. tp_normalise j.
-  tp_cmpxchg_suc j. tp_pure j (Snd _). by iFrame.
+  tp_pures j.
+  tp_cmpxchg_suc j. tp_normalise j.
+  tp_pures j. by iFrame.
 Qed.
 
 (* fork *)