diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 39f21d758b1be6aa9a7873f715b9b89832dcb966..6eaf109e165a6c201af66b34e84a8a945c963222 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -19,11 +19,11 @@ Tactic Notation "wp_expr_eval" tactic3(t) :=
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
-    eapply tac_wp_expr_eval;
-      [let x := fresh in intros x; t; unfold x; reflexivity|]
+    notypeclasses refine (tac_wp_expr_eval _ _ _ _ e _ _ _);
+      [let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
-    eapply tac_twp_expr_eval;
-      [let x := fresh in intros x; t; unfold x; reflexivity|]
+    notypeclasses refine (tac_twp_expr_eval _ _ _ _ e _ _ _);
+      [let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|]
   | _ => fail "wp_expr_eval: not a 'wp'"
   end.