diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 086fdd29412c66576439d35cc95dd3e2f59286ac..abb497d4f23c2c692150bf8ad2ab32775babbf6f 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -86,14 +86,14 @@ Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     wp_bind K; iApply lem; try iNext)
   | _ => fail "wp_apply: not a 'wp'"
   end.
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Alloc ?e =>
@@ -112,7 +112,7 @@ Tactic Notation "wp_alloc" ident(l) :=
   let H := iFresh in wp_alloc l as H.
 
 Tactic Notation "wp_load" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Load (Lit (LitLoc ?l)) =>
@@ -127,7 +127,7 @@ Tactic Notation "wp_load" :=
   end.
 
 Tactic Notation "wp_store" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Store ?l ?e =>
@@ -144,7 +144,7 @@ Tactic Notation "wp_store" :=
   end.
 
 Tactic Notation "wp_cas_fail" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | CAS ?l ?e1 ?e2 =>
@@ -162,7 +162,7 @@ Tactic Notation "wp_cas_fail" :=
   end.
 
 Tactic Notation "wp_cas_suc" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | CAS ?l ?e1 ?e2 =>
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 7f376360640d333c54522dc4a14b4afd25c4a8cf..9ebb7bb3df9d97299968f7967163067d615df566 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -26,7 +26,7 @@ Ltac wp_finish := intros_revert ltac:(
   rewrite -/of_val /= ?to_of_val; try strip_later; try wp_value_head).
 
 Tactic Notation "wp_value" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     wp_bind K; wp_value_head) || fail "wp_value: cannot find value in" e
   | _ => fail "wp_value: not a wp"
@@ -44,7 +44,7 @@ Tactic Notation "wp_rec" :=
   end.
 
 Tactic Notation "wp_lam" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with App ?e1 _ =>
 (*    match eval hnf in e1 with Rec BAnon _ _ => *)
@@ -57,7 +57,7 @@ Tactic Notation "wp_let" := wp_lam.
 Tactic Notation "wp_seq" := wp_let.
 
 Tactic Notation "wp_op" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
@@ -72,7 +72,7 @@ Tactic Notation "wp_op" :=
   end.
 
 Tactic Notation "wp_proj" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Fst _ => wp_bind K; etrans; [|eapply wp_fst; wp_done]; wp_finish
@@ -82,7 +82,7 @@ Tactic Notation "wp_proj" :=
   end.
 
 Tactic Notation "wp_if" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | If _ _ _ =>
@@ -93,7 +93,7 @@ Tactic Notation "wp_if" :=
   end.
 
 Tactic Notation "wp_case" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Case _ _ _ =>
@@ -105,7 +105,7 @@ Tactic Notation "wp_case" :=
   end.
 
 Tactic Notation "wp_focus" open_constr(efoc) :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match e' with
     | efoc => unify e' efoc; wp_bind K