From 66703789077fa86ac5de3afa11169bceebef0d00 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 29 Oct 2020 18:50:08 -0700 Subject: [PATCH] fix: `withIds` parser --- src/Lean/Parser/Tactic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index 4d4a59c51b..7892d12110 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -73,7 +73,7 @@ def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 match @[builtinTacticParser] def «match» := parser! nonReservedSymbol "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts @[builtinTacticParser] def «introMatch» := parser! nonReservedSymbol "intro " >> matchAlts -def withIds : Parser := optional (" with " >> many1 ident') +def withIds : Parser := optional (" with " >> many1 (checkColGt >> ident')) @[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds @[builtinTacticParser] def paren := parser! "(" >> seq1 >> ")" @[builtinTacticParser] def nestedTactic := tacticSeqBracketed