From f2f71a60281f66d78687128b8fb879e0f7a11fe0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 09:01:57 -0800 Subject: [PATCH] fix: Reset core message log --- Pantograph/Goal.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 52562e7..b140ee7 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -250,6 +250,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E return .some $ ← m.toString else return .none + Core.resetMessageLog if ¬ newMessages.isEmpty then return .failure newMessages.toArray return .success nextState