Commit 2023-01-17 03:10 e242a114
View on Github →feat: remove replaceAll option from to_additive (#1504) It was an option to disable the heuristics when implementing them in mathlib3. However, the heuristics now work quite well, and this flag is used 0 times in mathlib3 or mathlib4. If the heuristics don't work, we manually write down the additive declaration, so this option is useless.