I have a project where I use single precision floats, but no doubles.
Problem is, that printf processes all floating point values as doubles, even if the caller is content with single precision formatting. On devices without double-FPU, this pulls in __aeabi_dsub, __aeabi_dmul and the likes, which are several kilobytes large.

My suggestion is to add a compile option so that floating point values are formatted with single precision.

The value would still be passed as a double to printf, which would then be converted to float.
Some of the required functionality seems to be already there, via the #if DBL_MANT_DIG == 24 define.