diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 189b0e4970..371fbff579 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -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 diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 862953f547..37487bf03a 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -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