iIntros: bad error when trying to use a name that's already used
If there already is a variable x
in the context, running iIntros (x)
yields "No applicable tactic". That's not a very useful error, and it just took me a while to realize the actual problem. Is there a way to make this show the error generated by the underlying intros
?