Commit 2026-06-16 21:10 da24afce

chore: avoid meta-importing math files (#40671) It should never be neccessary to meta import a maths file, so this PR removes some such imports. In some cases this was caused by a public meta section at the top of a tactic file, even though there are some definitions in the file that should not be meta (because they are used as part of the generated proofs).