discard tactic_state after failure?

Stream: general

[Scott Morrison]

Is there an existing tactic that runs a tactic, then restores the original tactic_state if it fails?

[Patrick Massot]

try?

[Scott Morrison]

(I've run into a problem where failed tactics are having unwanted side effects, e.g. unifying metavariables.)

[Simon Hudon]

So you write try tac, tac unifies variables and then fails and the unification persists?

[Mario Carneiro]

try definitely restores the original tactic state after failure, so it's possible you've stumbled upon one of lean's less functional sides

[Scott Morrison]

Hmm, it seems I was wrong, as sticking such a tactic into the place I thought would fix things, hasn't fixed things. Maybe more later, sorry for the noise!