PR #18275: fix(tactic/core): plug leaks from `classical`

Stream: triage

[Random Issue Bot]

Today I chose PR 18275 for discussion!

fix(tactic/core): plug leaks from classical
Created by @Eric Wieser (@eric-wieser) on 2023-01-24
Labels: WIP, not-ready-to-merge

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

I think that's obsolete now that the tactic was rewritten in Lean 4. Can someone confirm?

[Mario Carneiro]

yes