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).
Merge request reports
Activity
Please register or sign in to reply