From b42d917aa70fa82ebf07d4480ecd14441e07eb23 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 17 Dec 2024 08:18:27 +0900
Subject: [PATCH] fix: Unnecessary instantiation call

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

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 6ff14d2..f573332 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -183,7 +183,8 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
   -- to one of these seed mvars, it means an error has occurred when a tactic
   -- was executing on `src`. `evalTactic`, will not capture these mvars, so we
   -- need to manually find them and save them into the goal list.
-  let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar src)
+
+  let descendants ←  Meta.getMVars (.mvar src)
   --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
   let mut alreadyVisited : MVarIdSet := {}
   let mut result : MVarIdSet := {}