[PHP-DOC] Re: ID change in docs

[Jeroen van Wolffelaar]

> Why? And why do you change it a minute after your announcement?

And on the why, because the type is 'float', and not 'double'.

PHP has no distinct floating point types, so 'float' is the one and only
right name for it. I discussed this with Zeev, and he agreed on that point.
And also: Double really gives the feeling there also needs to be some
'single' type...

Same goes for integer. We also don't call that long, because we happen to
use the C-type 'long' for it?

Jeroen