actuall make do_step work on heap_step goals

70fcbb3c · Ralf Jung · fb144483 · 70fcbb3c
Commit 70fcbb3c authored Feb 03, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

barrier/heap_lang_tactics.v barrier/heap_lang_tactics.v +3 -0

No files found.
--- 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.