fix Num.of_float for v1 branch, too

Essentially the same as for the master branch.