diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 096efe0117..54c4bb73d7 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -153,6 +153,7 @@ builtin_initialize register_parser_alias declVal register_parser_alias optDeclSig register_parser_alias openDecl + register_parser_alias docComment end Command