chore: report used instances correctly in diagnostics

2026-04-05 03:34:08 +00:00 · 2024-05-02 15:32:43 +10:00
1 changed files with 1 additions and 1 deletions
--- 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