Confusing error message for floating-point literals

theory T
  use ieee_float.Float32 as B32
  goal g : (1.:B32.t) = (1:B32.t)
end

gives Type t cannot be used for a numeric literal, which is wrong by definition.

Either the error message should be Invalid floating point literal: '1', or the code should just be modified to accept such a literal.