From 52ab8de201f9526e4752912d4ad475abae9b1875 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 23:05:26 +0100
Subject: [PATCH] Parenthesis bug in tactic. Thanks to Ralf for noting.
---
barrier/heap_lang_tactics.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/barrier/heap_lang_tactics.v b/barrier/heap_lang_tactics.v
index d8d086030..78fea003a 100644
--- a/barrier/heap_lang_tactics.v
+++ b/barrier/heap_lang_tactics.v
@@ -66,7 +66,7 @@ Ltac do_step tac :=
match goal with
| |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
reshape_expr e1 ltac:(fun K e1' =>
- eapply Ectx_step with K e1' _); [reflexivity|reflexivity|];
+ eapply Ectx_step with K e1' _; [reflexivity|reflexivity|];
first [apply alloc_fresh|econstructor];
- rewrite ?to_of_val; tac; fail
+ rewrite ?to_of_val; tac; fail)
end.
--
GitLab