iEval fails in strange ways when tactic creates new goals
Using iEval rewrite foo
when this opens new goals with side-conditions fails in very strange ways. The reason is that IPM runs unfold x; reflexivity
on all resulting goals.
The tricky part in resolving this will be figuring out which goal is the "original" one (side-conditions could be added before or after). But at least this simple cases can be improved a lot by checking whether x
is even present in the goal.