Commit 2025-12-05 13:19 a7e99551

feat(tauto): better error message on failure (#32406) This PR improves the tauto error message. Previously, it said "tauto failed to solve some goals.", and then a separate message reported on the unsolved goals. But I think these unsolved goals are implementation details of tauto. So instead, the error message now says "Tactic tauto failed", followed by the goal on which tauto was run. This change is so that tauto can be used as part of the by_contra! tactic.