From 4a18679c922d928c82e04251b90abb40d82e7b99 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Apr 2022 09:26:32 -0700 Subject: [PATCH] chore: include problematic `match` auxiliary declaration name in the error message --- src/Lean/Meta/Match/MatchEqs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 0791fdd28e8f..65f5eae573c1 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -289,7 +289,7 @@ where <|> (substSomeVar mvarId) <|> - (throwError "failed to generate equality theorems for `match` expression\n{MessageData.ofGoal mvarId}") + (throwError "failed to generate equality theorems for `match` expression `{matchDeclName}`\n{MessageData.ofGoal mvarId}") subgoals.forM (go ยท (depth+1))