remove pp change

kmill · kmill · commit b75ebe1d7278 · 2024-10-28T10:39:27.000-07:00
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -378,9 +378,6 @@ partial def delab : Delab := do
 
   let e ← getExpr
 
-  if ← getPPOption getPPAnalysisHole then
-    return ← `(_)
-
   if ← shouldOmitExpr e then
     return ← omission .deep
 
