--pool-type=int and double have now been merged into number.

BUG=v8:4280
LOG=N

Review URL: https://codereview.chromium.org/1717633002

Cr-Commit-Position: refs/heads/master@{#34164}