From c12fa6f0e28da33a4b4eacfedb8bc3abb9231043 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Jan 2022 12:58:03 -0800 Subject: [PATCH] fix: error message The equation theorems may fail for other reasons. --- 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 321240b8a2..64baad8643 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -158,7 +158,7 @@ where else throwError "spliIf failed") <|> - (throwError "failed to generate equality theorems for `match` expression, support for array literals has not been implemented yet\n{MessageData.ofGoal mvarId}") + (throwError "failed to generate equality theorems for `match` expression\n{MessageData.ofGoal mvarId}") subgoals.forM (go . (depth+1))