Skip to content

Use `simpl` in `wp_` tactics just in the expression

Robbert Krebbers requested to merge ci/robbert/simpl_local into master

This fixes #113 (closed). It is a bit hackish, but still seems like the most sane way of achieving this in Ltac.

Edited by Robbert Krebbers

Merge request reports