Skip to content

Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.

Robbert Krebbers requested to merge robbert/destruct_select into master

These tactics are consistent with existing tactics like revert select and rename select.

Merge request reports