Set Typeclasses Debug output is out of order

[Janno]

Description of the problem

Hints are printed only after they have been applied. Any debug output generated by the hint application itself (not via subgoals) is printed before the first mention of the hint. In case of anomalies, this means finding out which hint is responsible is difficult. And the output is just difficult to read, even when nothing goes wrong.

PR coming very soon.

Small Rocq / Coq file to reproduce the bug

Create HintDb foo.
Parameter bar cls : Prop.
Axiom c : cls.
Axiom hint : cls -> bar.
Hint Resolve c : foo.
Hint Extern 0 bar => let c := constr:(ltac:(typeclasses eauto with foo) :> cls) in exact (hint c) : foo.
Set Typeclasses Debug.
Goal bar.
Proof.
  typeclasses eauto with foo. (* [exact c] comes before the [Hint Extern] for [bar]. *)
(*
Debug: 1: looking for bar without backtracking
Debug: 1: looking for cls without backtracking
Debug: 1.1: exact c on cls, 0 subgoal(s)
Debug: 1.1: (*external*) (let c := constr:((ltac:(typeclasses eauto with foo) :> cls)) in
                                   exact (hint c)) on bar, 0 subgoal(s)
*)

Version of Rocq / Coq where this bug occurs

No response

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response