chore: reduce number of dependencies

@Kha Please try to avoid importing `Lean.Meta`, it is huge, and any
change there was forcing a bunch of files to be recompiled since
`Parser.Extension` depends on `Parenthesizer`
This commit is contained in:
Leonardo de Moura 2020-08-14 10:55:03 -07:00
parent 8e81c19162
commit d85a41a4d7
2 changed files with 4 additions and 2 deletions

View file

@ -14,7 +14,7 @@ emitting a token, we already know the text following it and can decide whether o
necessary.
-/
import Lean.Parser
import Lean.Meta
import Lean.Meta.ReduceEval
import Lean.Elab.Quotation
namespace Lean

View file

@ -70,7 +70,9 @@ node).
-/
import Lean.Meta
import Lean.Util.ReplaceExpr
import Lean.Meta.Basic
import Lean.Meta.WHNF
import Lean.KeyedDeclsAttribute
import Lean.Parser.Basic
import Lean.ParserCompiler