Commit d436e40c authored by Ralf Jung's avatar Ralf Jung

avoid by in tactics (as advised by Robbert)

parent df7a0a33
......@@ -4,12 +4,12 @@ Import uPred.
Ltac wp_strip_later :=
match goal with
| |- _, _ => let H := fresh in intro H; wp_strip_later; revert H
| |- _ _ => etransitivity; [|by apply later_intro]
| |- _ _ => etransitivity; [|solve [ apply later_intro] ]
end.
Ltac wp_bind K :=
lazymatch eval hnf in K with
| [] => idtac
| _ => etransitivity; [|by apply (wp_bind K)]; simpl
| _ => etransitivity; [|solve [ apply (wp_bind K) ]]; simpl
end.
Ltac wp_finish :=
let rec go :=
......
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