max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: error message

Browse source
This commit is contained in:
Sebastian Ullrich 2021-05-05 14:45:50 +02:00
parent a43dca0b9f
commit 76c66fc4d4
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Tactic/Basic.lean
View file

@ -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)