Improve some iIntros error messages
A failing iIntros for implications should prettify the identifier before printing, and iIntros on something that isn't a wand or implication should say what couldn't be introduced (to clarify that `iIntros "HP HQ"` failed because of the HQ in particular, for example).
Loading
Please register or sign in to comment