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.
wp_*
simpl
