• Tej Chajed's avatar
    Improve some iIntros error messages · 3732f05e
    Tej Chajed authored
    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).