max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: we don't want antiquotation for seq1

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-28 15:38:41 -07:00
parent 79078a03b6
commit aa410283c6
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Parser/Term.lean
View file

@ -30,7 +30,8 @@ def tacticSeq :=
nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented
/- Raw sequence for quotation and grouping -/
def seq1 := parser! sepBy1 tacticParser "; " true
def seq1 :=
node `Lean.Parser.Tactic.seq1 $ sepBy1 tacticParser "; " true
end Tactic