remove duplicated goals?

Stream: Is there code for X?

[Scott Morrison]

I remember somewhere a function that removes duplicated goals (i.e. the same MVarId, on the list twice!) It's easy to re-implement, but does anyone know where this lives?

[Alex J. Best]

I guess recover will already do this, I don't know of a different tactic to that though

[Alex J. Best]

So you can either put recover before the bad tactic, or recover skip after