Do not run `simpl` on user-visible goals
The proof mode, and in particular the wp_*
tactics, currently sometimes run simpl
on the user's goal. That can be annoying if simpl
misbehaves. Ideally, we should avoid running simpl
on user goals.
The proof mode, and in particular the wp_*
tactics, currently sometimes run simpl
on the user's goal. That can be annoying if simpl
misbehaves. Ideally, we should avoid running simpl
on user goals.