Fix type of the PHP_FLOAT_DIG constant

It used to be an int (https://github.com/php/php-src/pull/9616/files#diff-2978fe1c2c45b4eca89dc476376ddc7193bc4e5e7fff0c7d1c465f057b35a5e6L2155) before constant registration was refactored.

Author: kocsismate

main/main.stub.php

@@ -157,7 +157,7 @@
  */
 const PHP_FD_SETSIZE = UNKNOWN;
 /**
- * @var float
+ * @var int
  * @cvalue DBL_DIG
  */
 const PHP_FLOAT_DIG = UNKNOWN;