fix PPWithUniv

kmill · kmill · commit 68908a1390dd · 2023-12-17T10:12:26.000-05:00
diff --git a/Mathlib/Tactic/PPWithUniv.lean b/Mathlib/Tactic/PPWithUniv.lean
@@ -28,8 +28,7 @@ def delabWithUniv : Delab :=
     let expr := subExpr.expr
     let expr := mkAppN (expr.getAppFn.setOption pp.universes.name true) expr.getAppArgs
     { subExpr with expr }
-  withTheReader SubExpr enablePPUnivOnHead <|
-    delabAppImplicit <|> delabAppExplicit
+  withTheReader SubExpr enablePPUnivOnHead delabApp
 
 /--
 `attribute [pp_with_univ] Ordinal` instructs the pretty-printer to
