diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index ced5a06697f4..57abbf5eee85 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -909,14 +909,15 @@ abbrev declModifiersT := declModifiers true builtin_initialize register_parser_alias (kind := ``declModifiers) "declModifiers" declModifiersF register_parser_alias (kind := ``declModifiers) "nestedDeclModifiers" declModifiersT - register_parser_alias declId - register_parser_alias declSig - register_parser_alias declVal - register_parser_alias optDeclSig - register_parser_alias openDecl - register_parser_alias docComment - register_parser_alias plainDocComment - register_parser_alias visibility + register_parser_alias declId + register_parser_alias declSig + register_parser_alias declVal + register_parser_alias optDeclSig + register_parser_alias openDecl + register_parser_alias docComment + register_parser_alias plainDocComment + register_parser_alias visibility + register_parser_alias "optionValue" Command.optionValue /-- Registers an error explanation. diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58eddae..ad491b0de15a 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,3 +1,4 @@ +// update me! #include "util/options.h" namespace lean {