Commit 98f73a0b authored by Robbert Krebbers's avatar Robbert Krebbers

Perform a simpl after wp_apply.

wp_apply often results in an of_val that should be simplified.
parent f310c854
...@@ -222,7 +222,7 @@ Tactic Notation "wp_apply" open_constr(lem) := ...@@ -222,7 +222,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
iStartProof; iStartProof;
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind_core K; iApply lem; try iNext) wp_bind_core K; iApply lem; try iNext; simpl)
| _ => fail "wp_apply: not a 'wp'" | _ => fail "wp_apply: not a 'wp'"
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