diff --git a/barrier/heap_lang_tactics.v b/barrier/heap_lang_tactics.v index d8d086030f74edd48f66fc59b17bf6d2ee36e1f1..78fea003a287a19e60d15ca7b26827b81a92c35a 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.