From 698c3db6559da8e2475199c3bd595cfb162c1923 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 10 Oct 2020 07:41:44 -0700 Subject: [PATCH] chore: take `doSeq` at `initialize` --- src/Lean/Parser/Command.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 1ae4d3f2e7..f0439b3c18 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -88,7 +88,7 @@ def openSimple := parser! many1 ident @[builtinCommandParser] def «open» := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple) @[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notFollowedBy «end» >> commandParser) >> "end" -@[builtinCommandParser] def «initialize» := parser! "initialize " >> optional (ident >> Term.typeSpec >> Term.leftArrow) >> termParser +@[builtinCommandParser] def «initialize» := parser! "initialize " >> optional (ident >> Term.typeSpec >> Term.leftArrow) >> Term.doSeq @[builtinCommandParser] def «in» := tparser! " in " >> commandParser