Open dranov opened 7 months ago
There are two problems with this error message:
->
, mentioning the tactic rewrite
which the user didn't write themselves;To avoid this, we would need to write our own error message rather than rely on the one generated by the tactics used to implement ->
.
I would expect the
H
to not be there in the error message (it isn't there after the tactic fails), but this is not very important.