From 3ee9cdd2dcb7ee5b54941f3979fd7d5bdb7505f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 19 Sep 2020 16:12:57 -0700 Subject: [PATCH] doc: document issue @Kha One possible fix: we store `currNamespace` and `openDecls` at `CoreM`. The issue is similar to the one we had with the pretty printer. --- src/Lean/Elab/Util.lean | 2 +- stage0/src/Lean/Elab/Util.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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) <|>