Commit 2025-07-31 17:11 c53189a3
View on Github →feat(to_additive): improve (error) message of (reorder := ...) (#27692)
This PR improves the ease of use of (reorder := ...) for the to_dual tactic.
It also supersedes #27452, by removing the unneeded List.reverse.