diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index 26a452e663..9241d66d0b 100644 --- a/src/Lean/Elab/Util.lean +++ b/src/Lean/Elab/Util.lean @@ -72,7 +72,7 @@ match attrParamSyntaxToIdentifier arg with | some k => checkSyntaxNodeKind env k <|> - checkSyntaxNodeKindAtNamespaces env k env.getNamespaces + checkSyntaxNodeKindAtNamespaces env k env.getNamespaces -- TODO: fix for the new frontend. We do not store the current namespaces and OpenDecls in the environment <|> checkSyntaxNodeKind env (defaultParserNamespace ++ k) <|> diff --git a/stage0/src/Lean/Elab/Util.lean b/stage0/src/Lean/Elab/Util.lean index 26a452e663..9241d66d0b 100644 --- a/stage0/src/Lean/Elab/Util.lean +++ b/stage0/src/Lean/Elab/Util.lean @@ -72,7 +72,7 @@ match attrParamSyntaxToIdentifier arg with | some k => checkSyntaxNodeKind env k <|> - checkSyntaxNodeKindAtNamespaces env k env.getNamespaces + checkSyntaxNodeKindAtNamespaces env k env.getNamespaces -- TODO: fix for the new frontend. We do not store the current namespaces and OpenDecls in the environment <|> checkSyntaxNodeKind env (defaultParserNamespace ++ k) <|>