diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 283442f023..ddbecce413 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -867,6 +867,7 @@ builtin_initialize register_parser_alias optDeclSig register_parser_alias openDecl register_parser_alias docComment + register_parser_alias visibility /-- Registers an error explanation.