fix: declModifiers syntax kind

leanprover · Jun 28, 2022 · c64ac02 · c64ac02
1 parent a9cc57c
commit c64ac02
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 8 deletions.
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
@@ -143,13 +143,13 @@ def openDecl         := openHiding <|> openRenaming <|> openOnly <|> openSimple
 @[runBuiltinParserAttributeHooks] abbrev declModifiersT := declModifiers true
 
 builtin_initialize
-  register_parser_alias "declModifiers"       declModifiersF
-  register_parser_alias "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 (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
 
 end Command
 

diff --git a/tests/lean/run/lemma.lean b/tests/lean/run/lemma.lean
@@ -1,4 +1,4 @@
-macro "lemma" n:declId sig:declSig val:declVal : command => `(theorem $n $sig $val)
+macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command => `($mods:declModifiers theorem $n $sig $val)
 
 lemma fooSimple (n : Nat) : Prop :=
   if n = 0 then True else False