Commit 2024-05-14 17:58 56dc11ac

chore: deprecate @[pp_dot] (#12609) Now that we're on Lean v4.8.0-rc1, there's no need for @[pp_dot] due to the new pp.fieldNotation.generalized feature. This PR removes all uses of @[pp_dot] and makes it emit a warning that it's been deprecated. The new feature does not pretty print proof terms with dot notation, so there is a small regression for Eq.symm, Eq.trans, and, sometimes, False.elim. However, pp.proofs is false by default.