diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 361b83a3a61a055095cf72f16f8c079a77a0a698..e84f90afecc010c45cfba8082db4859028aaaebc 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -82,7 +82,7 @@ Tactic Notation "wp_seq" := wp_let.
 Tactic Notation "wp_op" :=
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
+    lazymatch eval hnf in e' with
     | BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
     | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
     | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish