Skip to content

Improve some iIntros error messages

Tej Chajed requested to merge tchajed/iris-coq:fix-intros-errors into master

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