From 9d1f2b644f21f658ad2855e9e5746ff2fe0d2003 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 Sep 2020 07:05:38 -0700 Subject: [PATCH] chore: rwRuleSeq `;` => `,` --- 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 13b534c850..9201aee962 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -56,7 +56,7 @@ def location := parser! "at " >> (locationWildcard <|> locationTarget <| @[builtinTacticParser] def changeWith := parser! nonReservedSymbol "change " >> termParser >> " with " >> termParser >> optional location def rwRule := parser! optional (unicodeSymbol "←" "<-") >> termParser -def rwRuleSeq := parser! "[" >> sepBy1 rwRule "; " true >> "]" +def rwRuleSeq := parser! "[" >> sepBy1 rwRule ", " true >> "]" @[builtinTacticParser] def «rewrite» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRule >> optional location @[builtinTacticParser] def «rewriteSeq» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRuleSeq >> optional location