See https://github.com/coq/coq/pull/17648#issuecomment-1568700456 . This MR simply removes the offending test because the test has already caused problems previously (!421 (merged)) and does not seem that useful.