From e13613d6331edb166b997ce5d59cf435f241eee2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 May 2024 15:47:51 +1000 Subject: [PATCH] chore: report used instances correctly in diagnostics (#4049) --- src/Lean/Meta/Diagnostics.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Diagnostics.lean b/src/Lean/Meta/Diagnostics.lean index baf77a8ef3..1bf034fe42 100644 --- a/src/Lean/Meta/Diagnostics.lean +++ b/src/Lean/Meta/Diagnostics.lean @@ -58,7 +58,7 @@ def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM Dia getReducibilityStatusCore env declName matches .reducible def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do - mkDiagSummary (← get).diag.heuristicCounter + mkDiagSummary (← get).diag.instanceCounter def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) : MessageData := if s.isEmpty then