From faa612e7b79a00c85eef899b72d38535928c7553 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 17 Oct 2022 16:05:42 -0400 Subject: [PATCH] chore: remove `#resolve_name` --- src/Lean/Parser/Command.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 199095477a..79443f6e9f 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -130,7 +130,6 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «opaque» <| @[builtinCommandParser] def exit := leading_parser "#exit" @[builtinCommandParser] def print := leading_parser "#print " >> (ident <|> strLit) @[builtinCommandParser] def printAxioms := leading_parser "#print " >> nonReservedSymbol "axioms " >> ident -@[builtinCommandParser] def «resolve_name» := leading_parser "#resolve_name " >> ident @[builtinCommandParser] def «init_quot» := leading_parser "init_quot" def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit @[builtinCommandParser] def «set_option» := leading_parser "set_option " >> ident >> ppSpace >> optionValue