max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: document issue

Browse source 
@Kha One possible fix: we store `currNamespace` and `openDecls` at `CoreM`.
The issue is similar to the one we had with the pretty printer.
This commit is contained in:
Leonardo de Moura 2020-09-19 16:12:57 -07:00
parent 3e42dac1ee
commit 3ee9cdd2dc
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Util.lean
View file

@ -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)
<|>

2
stage0/src/Lean/Elab/Util.lean generated
View file

@ -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)
<|>