From 1f183cdc305c81fff99734a43ea5b87093a6a22f Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Fri, 30 Jul 2021 11:37:21 -0700 Subject: [PATCH] fix: only pp.analyze when all is not set --- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 1ea188c4c5..d2f49e9247 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -391,7 +391,7 @@ def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (options catch _ => pure () let e ← if getPPInstantiateMVars opts then ← Meta.instantiateMVars e else e let optionsPerPos ← - if getPPAnalyze opts && optionsPerPos.isEmpty then + if !getPPAll opts && getPPAnalyze opts && optionsPerPos.isEmpty then topDownAnalyze e else optionsPerPos catchInternalId Delaborator.delabFailureId