From 2c54a0d17a8a558e6d8d79e7d5d6281ffdf30e2d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 5 Apr 2022 17:28:45 +0200 Subject: [PATCH] feat: allow anonymous antiquotations for `tacticSeq` --- src/Lean/Parser/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index d0590847ab..7bdf08f362 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -36,7 +36,7 @@ def tacticSeq1Indented : Parser := def tacticSeqBracketed : Parser := leading_parser "{" >> many (group (ppLine >> tacticParser >> optional ";")) >> ppDedent (ppLine >> "}") def tacticSeq := - leading_parser (withAnonymousAntiquot := false) tacticSeqBracketed <|> tacticSeq1Indented + leading_parser tacticSeqBracketed <|> tacticSeq1Indented /- Raw sequence for quotation and grouping -/ def seq1 :=