remove usages of to-be-deprecated float consts#4903

RalfJung merged 1 commit intorust-lang:masterrust-lang/miri:masterfrom

cyrgani:no-old-floatscyrgani/miri:no-old-floatsCopy head branch name to clipboard