This lets us make progress in !376 (merged).
Sounds fine to me.
This version of Coq is ancient, nobody replied in the chat saying they still need it, Iris dropped this a while ago, and we waited 2 days... I think that's enough caution.
merged
mentioned in commit b7a5fed7