From 02a8a2435a0aa6641011ae108c75007ea98eaed6 Mon Sep 17 00:00:00 2001
From: Peiyang Song <p_song@ucsb.edu>
Date: Wed, 13 Mar 2024 20:47:37 -0700
Subject: [PATCH] Minor fix for frontend thanks to Patrick Massot

---
 LeanCopilot/Frontend.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/LeanCopilot/Frontend.lean b/LeanCopilot/Frontend.lean
index f576192..1148ede 100644
--- a/LeanCopilot/Frontend.lean
+++ b/LeanCopilot/Frontend.lean
@@ -27,7 +27,8 @@ def suggestion (tac : String) (msgs : MessageLog := {}) : TacticM Suggestion :=
   let postInfo? ← if goals.isEmpty then pure none else
     let mut str := "\nRemaining subgoals:"
     for g in goals do
-      let e ← PrettyPrinter.ppExpr (← instantiateMVars (← g.getType))
+      let goalType ← instantiateMVars (← g.getType)
+      let e ← g.withContext do (PrettyPrinter.ppExpr goalType)
       str := str ++ Format.pretty ("\n⊢ " ++ e)
     pure (some str)
   let style? := if goals.isEmpty then some .success else none