Commit 2024-05-10 12:00 8d93a534

chore: compatibility with Lean incrementality branch (#12796) Backward-compatible fixes for leanprover/lean4#3940. In particular, gets rid of two open private (out of six in all of Mathlib) which in my opinion really were not necessary and just invited breakage. Somehow the unused variables and unnecessary have linters became more complete, which might be due to earlier mvar instantiation in Elab.MutualDef but I haven't investigated deeply.