DELETE HISTORY ignores indices

CREATE TABLE t2 (x INT,

`start_time` timestamp(6) GENERATED ALWAYS AS ROW START,

`end_time` timestamp(6) GENERATED ALWAYS AS ROW END,

   PERIOD FOR SYSTEM_TIME (`start_time`, `end_time`)

 ) ENGINE=InnoDB DEFAULT CHARSET=utf8 WITH SYSTEM VERSIONING

  PARTITION BY SYSTEM_TIME 

 (PARTITION `p_hist` HISTORY ENGINE = InnoDB,

  PARTITION `p_cur` CURRENT ENGINE = InnoDB);

ALTER TABLE t2 ADD INDEX `startendtime` (`start_time`, `end_time`);

MariaDB [test]> explain SELECT * FROM t2 FOR SYSTEM_TIME FROM '2016-01-01 00:00:00' TO '2017-01-01 00:00:00';

+------+-------------+-------+-------+---------------+--------------+---------+------+------+-------------+

| id   | select_type | table | type  | possible_keys | key          | key_len | ref  | rows | Extra       |

+------+-------------+-------+-------+---------------+--------------+---------+------+------+-------------+

|    1 | SIMPLE      | t2    | range | startendtime  | startendtime | 7       | NULL | 2    | Using where |

+------+-------------+-------+-------+---------------+--------------+---------+------+------+-------------+

1 row in set (0.002 sec)

MariaDB [test]> explain DELETE HISTORY FROM t2 BEFORE SYSTEM_TIME '2016-10-09 08:07:06';

+------+-------------+-------+------+---------------+------+---------+------+------+-------------+

| id   | select_type | table | type | possible_keys | key  | key_len | ref  | rows | Extra       |

+------+-------------+-------+------+---------------+------+---------+------+------+-------------+

|    1 | SIMPLE      | t2    | ALL  | NULL          | NULL | NULL    | NULL | 2    | Using where |

+------+-------------+-------+------+---------------+------+---------+------+------+-------------+

1 row in set (0.001 sec)