From cb87fcd9dd89fdeaaaad49f0dd0111b4e7416c49 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 00:16:52 -0800 Subject: [PATCH] fix: Insert `mvarDeps` --- Pantograph/Goal.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 7a09435..52562e7 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -184,6 +184,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) -- 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 _ ← Elab.Term.logUnassignedUsingErrorInfos descendants let mut alreadyVisited : MVarIdSet := {} let mut result : MVarIdSet := {} for { mvarId, .. } in (← get).mvarErrorInfos do @@ -191,9 +192,9 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) alreadyVisited := alreadyVisited.insert mvarId /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or delayed assigned to another metavariable that is unassigned. -/ - let mvarDeps ← Meta.getMVars (mkMVar mvarId) + let mvarDeps ← Meta.getMVars (.mvar mvarId) if mvarDeps.any descendants.contains then do - result := result.insert mvarId + result := mvarDeps.foldl (·.insert ·) result return result.toList private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=