chore: report used instances correctly in diagnostics (#4049)

leanprover · May 2, 2024 · e13613d · e13613d
1 parent 5f1c4df
commit e13613d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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