From 7b221fa8e865daad467bbf675f078e95b858251e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Jan 2017 13:02:02 +0100
Subject: [PATCH] Use lazymatch in reshape_val, it should not backtrack.

---
 theories/heap_lang/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 8a448ec29..1c040a947 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)
-- 
GitLab