Commit 2026-07-07 08:33 cfa16a74
View on Github →chore: remove redundant open Classical in (#41387)
Hopefully all of them. Also this PR moves the "open Classical in" to the proof ("classical" in tactic proofs) whenever possible.
chore: remove redundant open Classical in (#41387)
Hopefully all of them. Also this PR moves the "open Classical in" to the proof ("classical" in tactic proofs) whenever possible.