From ed67bd56e0ae6ef3b70666bc741014575e4b6ccc Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Sat, 31 Jul 2021 15:07:43 -0700
Subject: [PATCH] fix: only unexpand when pp.notation=true

---
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index c6c2e35599..bab72bf3f0 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -251,7 +251,7 @@ def delabAppImplicit : Delab := do
         | some stx => argStxs.push stx
       pure (fnStx, paramKinds.tailD [], argStxs))
   let stx := Syntax.mkApp fnStx argStxs
-  if ← isRegularApp then
+  if ← isRegularApp <&&> getPPOption getPPNotation then
     unexpandRegularApp stx
     <|> unexpandStructureInstance stx
     <|> unexpandCoe stx