From 76c66fc4d49f8d9ababa603880a905b9c88a9856 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 5 May 2021 14:45:50 +0200
Subject: [PATCH] fix: error message

---
 src/Lean/Elab/Tactic/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 91cb1ab6cc..a5fa4501af 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -144,7 +144,7 @@ mutual
           match table.find? k with
           | some evalFns => evalTacticUsing s stx evalFns
           | none         => expandTacticMacro stx
-      | _ => throwError "unexpected command"
+      | _ => throwError m!"unexpected tactic{indentD stx}"
 
   partial def evalTactic (stx : Syntax) : TacticM Unit :=
     withTacticInfoContext stx (evalTacticAux stx)