diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 8a047e571ff2b1b64131cf04b4020763eae2e9b0..677aa60634ba8c6f1518ab3dcd199e846caffd21 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -66,10 +66,9 @@ Ltac wp_bind_core K :=
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
-    match e' with
-    | efoc => unify e' efoc; wp_bind_core K
-    end) || fail "wp_bind: cannot find" efoc "in" e
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
+    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
+    || fail "wp_bind: cannot find" efoc "in" e
   | _ => fail "wp_bind: not a 'wp'"
   end.