Adapt to https://github.com/coq/coq/pull/16788

This is backward compatible so can be merged before the parent PR https://github.com/coq/coq/pull/16788

Thanks! I can't say I understand why this helps, but sure, nothing wrong with having a space there.

merged

mentioned in commit 94d782ad

mentioned in commit 026c3af0