What happens if I drop a MySQL column without dropping its index first?

With one of my MySQL tables, I dropped colu开发者_如何转开发mn col1 before I drop it from a unique index (col0, col1, col2, col3) that contains it.

Is it automatically taken care of by MySQL? It seems the unique index that was previously (col0, col1, col2, col3) was automatically changed to (col0, col2, col3) after I deleted the column col1.

Is it going to be a problem or do I have to drop the unique index and re-create it as (col0, col2, col3)?

According to the MySQL 5.1 Reference Manual:

If columns are dropped from a table, the columns are also removed from any index of which they are a part. If all columns that make up an index are dropped, the index is dropped as well. If you use CHANGE or MODIFY to shorten a column for which an index exists on the column, and the resulting column length is less than the index length, MySQL shortens the index automatically.