From ab046db6eddc71ebae67e9eb4ec068f4fe7601b1 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Sep 2020 13:34:26 +0200
Subject: [PATCH] feat: prettify mvars somewhat

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

diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 3b6e05ee6b..35998eb386 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -247,6 +247,7 @@ pure $ mkIdent l.userName
 @[builtinDelab mvar]
 def delabMVar : Delab := do
 Expr.mvar n _ ← getExpr | unreachable!;
+let n := n.replacePrefix `_uniq `m;
 `(?$(mkIdent n))
 
 @[builtinDelab sort]