mentioned in commit a9f247da
merged
Won't this break things on older Coq?
We should also still be compatible with 8.20, at least.
Ah, there's a later commit that reverts this part. :)
