Commit 2026-07-08 09:06 ed0d70fd

chore: remove redundant open scoped Classical (#41423) This PR removes all redundant/unused open scoped Classical in. Furthermore, if the open scoped Classical is only needed for the proof of a declaration, it moves it there (and convert it to classical when in tactic mode). Excludes MathlibTest. This was done with a script bruteforcing everything, made by Claude code. Only thing remaining would be to check if all classical are really needed, but there are quite a lot of them (>3k).