fix: only unexpand when pp.notation=true

This commit is contained in:
Daniel Selsam 2021-07-31 15:07:43 -07:00 committed by Sebastian Ullrich
parent 4c41142a61
commit ed67bd56e0

View file

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