diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 011642e0ab..e890ffac17 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -297,6 +297,8 @@ def macroLastArg := macroDollarArg <|> macroArg @[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> incQuotDepth (parserOfStack 1) >> ")" +@[builtinTermParser] def dotIdent := leading_parser "." >> checkNoWsBefore >> ident + end Term @[builtinTermParser default+1] def Tactic.quot : Parser := leading_parser "`(tactic|" >> incQuotDepth tacticParser >> ")"