From 70fcbb3cf0c4f3fa39f59e7b002d4dba33bb3961 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 Feb 2016 14:04:16 +0100
Subject: [PATCH] actuall make do_step work on heap_step goals
---
barrier/heap_lang_tactics.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/barrier/heap_lang_tactics.v b/barrier/heap_lang_tactics.v
index 87e9f7a9d..f0219d72a 100644
--- a/barrier/heap_lang_tactics.v
+++ b/barrier/heap_lang_tactics.v
@@ -83,4 +83,7 @@ Ltac do_step tac :=
eapply Ectx_step with K e1' _; [reflexivity|reflexivity|];
first [apply alloc_fresh|econstructor];
rewrite ?to_of_val; tac; fail)
+ | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
+ first [apply alloc_fresh|econstructor];
+ rewrite ?to_of_val; tac; fail
end.
--
GitLab