C.axioms_ appears when printing

[Tragicus]

The axioms_ record of a structure C is hidden behind a notation. However, when printing, the notation does not print C, as in

From HB Require Import structures.

HB.mixin Record isC (T : Type) := {}.
HB.structure Definition C := {T of isC T}.

Check (C _).

which prints

C.axioms_ ?T
     : Type
where
?T : [ |- Type]

[CohenCyril]

I wonder how much of a bug of Coq this is.