max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: missing instantiateMVars

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-07 11:34:21 -08:00
parent 8e7c719ee8
commit 62bdbba78d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Util/Message.lean
View file

@ -63,7 +63,7 @@ partial def formatAux : Option MessageDataContext → MessageData → Format
| some ctx, ofSyntax s => s.formatStx (getSyntaxMaxDepth ctx.opts)
| none, ofSyntax s => s.formatStx
| none, ofExpr e => format (toString e)
| some ctx, ofExpr e => ppOld ctx.env ctx.mctx ctx.lctx ctx.opts e -- TODO: replace with new pretty printer
| some ctx, ofExpr e => ppOld ctx.env ctx.mctx ctx.lctx ctx.opts (ctx.mctx.instantiateMVars e).1 -- TODO: replace with new pretty printer
| _, withContext ctx d => formatAux (some ctx) d
| ctx, tagged cls d => Format.sbracket (format cls) ++ " " ++ formatAux ctx d
| ctx, nest n d => Format.nest n (formatAux ctx d)