Use `simpl` in `wp_` tactics just in the expression
This fixes #113 (closed). It is a bit hackish, but still seems like the most sane way of achieving this in Ltac.
This fixes #113 (closed). It is a bit hackish, but still seems like the most sane way of achieving this in Ltac.