diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index 93ac937869..cb841577c6 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -11,6 +11,7 @@ namespace Tactic builtin_initialize register_parser_alias tacticSeq + register_parser_alias tacticSeqIndentGt /- This is a fallback tactic parser for any identifier which exists only to improve syntax error messages.