WL#12575: Deprecate AUTO_INCREMENT on DOUBLE and FLOAT

MySQL supports AUTO_INCREMENT on DOUBLE and FLOAT columns. This has several 
weird behaviors and should be deprecated/removed.

Example 1:

  mysql> CREATE TABLE t1 (col1 FLOAT PRIMARY KEY AUTO_INCREMENT);
  Query OK, 0 rows affected (0.02 sec)
  mysql> INSERT INTO t1 VALUES (0.1), (0.2), (0.3), (0.4), (0.5), (0.4), (0.3),
 (0.2), (0.1);
  Query OK, 9 rows affected (0.00 sec)
  Records: 9 Duplicates: 0 Warnings: 0
  mysql> SELECT * FROM t1;
  +------+
  | col1 |
  +------+
  |    1 |
  |    2 |
  |    3 |
  |    4 |
  |    5 |
  |    6 |
  |    7 |
  |    8 |
  |    9 |
  +------+
  9 rows in set (0.00 sec)

Example 2:

  mysql> CREATE TABLE t1 (col1 FLOAT NOT NULL AUTO_INCREMENT PRIMARY KEY, col2 
INT) AUTO_INCREMENT=16777216;
  Query OK, 0 rows affected (0.03 sec)

  mysql> insert into t1 (col2) select 1;
  Query OK, 1 row affected (0.01 sec)
  Records: 1  Duplicates: 0  Warnings: 0

  mysql> insert into t1 (col2) select 1;
  ERROR 1062 (23000): Duplicate entry '16777200' for key 'PRIMARY'

F-1: Creating a table with a DOUBLE or FLOAT column declared as AUTO_INCREMENT 
shall give a deprecation warning.

F-2: Adding a DOUBLE or FLOAT column declared as AUTO_INCREMENT to an existing 
table shall give a deprecation warning.

F-3: Modifying an existing column to make it an AUTO_INCREMENT DOUBLE or FLOAT 
column shall give a deprecation warning.

The deprecation warning message is:
"AUTO_INCREMENT support for FLOAT/DOUBLE columns is deprecated and will be removed 
in a future release. Consider removing AUTO_INCREMENT from column '[column name]'.