diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 8a448ec295016679df4fb37362b4db77aadfa2b3..1c040a9472665570c95a71ed86f0c904d8ba720c 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -252,7 +252,7 @@ evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
 for each possible decomposition until [tac] succeeds. *)
 Ltac reshape_val e tac :=
   let rec go e :=
-  match e with
+  lazymatch e with
   | of_val ?v => v
   | Rec ?f ?x ?e => constr:(RecV f x e)
   | Lit ?l => constr:(LitV l)