convert, refl

Stream: general

[Reid Barton]

This is a new one for me--convert left a goal which I could close with refl

[Patrick Massot]

You can easily play with convert and, especially congr' code, they are easy to understand, as long as you don't try to understand what congr_core is doing, which I suspect you won't need to try

[Reid Barton]

Maybe refl closed some later goal, fixing a metavariable, and that caused an earlier goal to also be closable by refl

[Reid Barton]

I do have a _ in the argument to convert