Commit 2025-11-05 13:09 e96f0335

refactor(TacticAnalysis): use full CommandElabM context in test (#29771) Running the rwMerge linter on the whole of Mathlib reveals that the tactic analysis framework did not always correctly pass the environment to the test step of a pass. By running the test in a full CommandElabM and adding a ContextInfo and TacticInfo, we can access the right environment (using the ctxI.runTacticCode function). There are still a few subtle issues to do with notation but I would like to get this fix in first, since it involves some larger refactors.