Typeclass debug logs show misleading information about what happens to the proof state

[RalfJung]

In #16893 (comment) I learned that when the typeclass log says simple apply finite_countable ; trivial, that does not match what it actually does: instead of trivial it uses some internal-only tactic. Similarly, the simple apply part also does not match reality to my knowledge; for instance, typeclass resolution will use different unification settings to respect Typeclasses Opaque.

This should be fixed. Either the typeclass log should output tactics that actually match what happens, or it should output text that does not look like a tactic. The current situation means people debugging TC issues will copy-paste the tactic output from TC search into the Coq buffer to try and replay part of the search, and debug things at a particular point after a few lemmas have been applied -- only to be terribly confused because this does not actually properly replay the search. Basically Coq is printing things that are almost but not quite true, and that's the worst kind of wrong when you are trying to learn what happens in the middle of a big TC resolution.