Change floating pt number typename from $float to $double because that is the more
common understanding of what it is (esp. since most float imps are 4 bytes!)