diff --git a/barrier/heap_lang_tactics.v b/barrier/heap_lang_tactics.v
index 87e9f7a9d9ed9506e7beda5c8494a3f3e5e37fd9..f0219d72a89a76d11fdbaa0b6e7e952113c37d22 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.