`Hint Constants Transparent` is ignored for head constant

[jfehrle]

Description of the problem

auto et al don't unfold transparent head constants. It seems that they should--or be noted as an exception in the documentation.

FYI: @andres-erbsen

Small Rocq / Coq file to reproduce the bug

Definition Tru := True.

Create HintDb db.
Hint Constants Transparent : db.
Hint Resolve I : db.
Axiom myeq: True = True.
Hint Resolve myeq : db.
Print HintDb db.
(*  For XXX -> indicates XXX is the head constant
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
Unfoldable projection definitions: all
Cut: emp
For any goal ->   
For True ->   exact I (cost 0, pattern True, id 0)
For eq ->   exact myeq (cost 0, pattern True = True, id 0)
*)

Goal Tru.
  Fail progress auto with db. (* has failed with: Failed to progress *)
Abort.
  
Goal Tru = True. 
  progress info_auto with db.  (* works *)

Version of Rocq / Coq where this bug occurs

9.2