From b5d4e0a2fda53bed45b69a01d6120e018826414a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 22 Jul 2019 19:07:43 -0700 Subject: [PATCH] chore(library/init/lean/elaborator/basic): improve cryptic error message --- library/init/lean/elaborator/basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean index f3560af7b7..35fa0cde4f 100644 --- a/library/init/lean/elaborator/basic.lean +++ b/library/init/lean/elaborator/basic.lean @@ -264,8 +264,8 @@ stx.ifNode let k := n.getKind; match tables.find k with | some elab => elab n - | none => logError stx ("command elaborator failed, no support for syntax '" ++ toString k ++ "'")) - (fun _ => logErrorUsingCmdPos ("command elaborator failed, unexpected syntax")) + | none => logError stx ("command '" ++ toString k ++ "' has not been implemented")) + (fun _ => logErrorUsingCmdPos ("unexpected command")) structure FrontendState := (elabState : ElabState)