From 4380fe088d42dbeac27e4d0b2346d6abc247b823 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 17 Dec 2021 23:53:06 +0100
Subject: [PATCH] feat: Sanitize Syntax

---
 DocGen4/Process.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 00321f0..51ec4ff 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -86,6 +86,7 @@ structure Module where
 def prettyPrintTerm (expr : Expr) : MetaM InfoSyntax := do
   let ((expr, _), _) ← Elab.Term.TermElabM.run $ Elab.Term.levelMVarToParam (←instantiateMVars expr)
   let (stx, info) ← delabCore Name.anonymous [] expr
+  let stx := sanitizeSyntax stx |>.run' { options := ←getOptions }
   (←parenthesizeTerm stx, info)
 
 def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do