chore: include problematic match auxiliary declaration name in the …

…error message
leanprover · Apr 20, 2022 · 4a18679 · 4a18679
1 parent e1fbfb6
commit 4a18679
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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))