Use of float vs double in timevar

[Matt Austern]

Struct timevar_time_def has three members, all of type float.
Why float, instead of double?

Lots of platforms, including Apple's, can give you 64 bits
of timing information.  A float typically just has 24 bits of
mantissa.   As one of our hardware performance people
pointed out, this means that under some plausible
circumstances your precision will be worse than 1/8 sec.

Wouldn't it makes more sense to use double?

			--Matt