From 21d4658da8f5626a4849396faac69127515de9cc Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Wed, 11 Jan 2017 11:58:33 +0100
Subject: [PATCH] Correct a bug in reshape_expr.
---
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 9d3cd281b..8a448ec29 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -260,7 +260,7 @@ Ltac reshape_val e tac :=
let v1 := go e1 in let v2 := go e2 in constr:(PairV v1 v2)
| InjL ?e => let v := go e in constr:(InjLV v)
| InjR ?e => let v := go e in constr:(InjRV v)
- end in let v := go e in first [tac v | fail 2].
+ end in let v := go e in tac v.
Ltac reshape_expr e tac :=
let rec go K e :=
--
GitLab