Labels written on variables are lost
For example, with module:
module A
goal G : forall x. x = [@bouh] x
end
the label over variable "x" does not show in IDE, and can be checked (using transformations) to be absent from the internal representation as well.