Commit 52ab8de2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Parenthesis bug in tactic. Thanks to Ralf for noting.

parent 58a354a9
...@@ -66,7 +66,7 @@ Ltac do_step tac := ...@@ -66,7 +66,7 @@ Ltac do_step tac :=
match goal with match goal with
| |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef => | |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
reshape_expr e1 ltac:(fun K e1' => 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]; first [apply alloc_fresh|econstructor];
rewrite ?to_of_val; tac; fail rewrite ?to_of_val; tac; fail)
end. end.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment