stack overflow in refine

Stream: lean4

[Mario Carneiro]

example : True := by refine ?a; refine ?a

I was hoping that both refines would act like skip here except for tagging the new goal as case a, but the second one seems to end up being self referential and leads to a loop somewhere.

[Leonardo de Moura]

Pushed a fix for this.