diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 90e561f2fb320740831868db8f416b729b4b42c4..eb9ef069b83dad24a299e4cdf97a0232d957b92c 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -483,7 +483,7 @@ Tactic Notation "wp_cas_fail" :=
     |solve_mapsto ()
     |try congruence
     |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
-    |simpl; try wp_value_head]
+    |wp_expr_simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_fail _ _ _ _ K))
@@ -510,7 +510,7 @@ Tactic Notation "wp_cas_suc" :=
     |pm_reflexivity
     |try congruence
     |try fast_done (* vals_cas_compare_safe *)
-    |simpl; try wp_value_head]
+    |wp_expr_simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))