dunfold timeout

Stream: general

[Eric Wieser]

I'm getting a timeout in branch#eric-wieser/dunfold-timeout in a dunfold bad_type tactic on this line. What on earth is going on here?

[Kevin Buzzard]

yeah that's weird. I thought that dunfold bad_type was basically dsimp only [bad_type] or maybe dsimp only [bad_type.equations._eqn_1] but these work fine. Note that delta bad_type also works fine.