From 7a556d8f615a45f135873edbfc0a45bd3834ea12 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 8 Feb 2020 18:47:38 -0800
Subject: [PATCH] fix: use metavariable local context

---
 src/Init/Lean/Meta/Tactic/Util.lean | 3 +--
 src/Init/Lean/Util/PPGoal.lean      | 3 ++-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Init/Lean/Meta/Tactic/Util.lean b/src/Init/Lean/Meta/Tactic/Util.lean
index cd8c55378e..cb8883fe83 100644
--- a/src/Init/Lean/Meta/Tactic/Util.lean
+++ b/src/Init/Lean/Meta/Tactic/Util.lean
@@ -30,9 +30,8 @@ pure mvarDecl.type
 def ppGoal (mvarId : MVarId) : MetaM Format := do
 env  ← getEnv;
 mctx ← getMCtx;
-lctx ← getLCtx;
 opts ← getOptions;
-pure $ ppGoal env mctx lctx opts mvarId
+pure $ ppGoal env mctx opts mvarId
 
 @[init] private def regTraceClasses : IO Unit :=
 registerTraceClass `Meta.Tactic
diff --git a/src/Init/Lean/Util/PPGoal.lean b/src/Init/Lean/Util/PPGoal.lean
index c264797706..1207f044b1 100644
--- a/src/Init/Lean/Util/PPGoal.lean
+++ b/src/Init/Lean/Util/PPGoal.lean
@@ -8,11 +8,12 @@ import Init.Lean.Util.PPExt
 
 namespace Lean
 
-def ppGoal (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (mvarId : MVarId) : Format :=
+def ppGoal (env : Environment) (mctx : MetavarContext) (opts : Options) (mvarId : MVarId) : Format :=
 match mctx.findDecl? mvarId with
 | none          => "unknown goal"
 | some mvarDecl =>
   let indent := 2; -- Use option
+  let lctx   := mvarDecl.lctx;
   let pp (e : Expr) : Format := ppExpr env mctx lctx opts e;
   let instMVars (e : Expr) : Expr := (mctx.instantiateMVars e).1;
   let addLine (fmt : Format) : Format := if fmt.isNil then fmt else fmt ++ Format.line;