Note that this requires dropping support for Coq 8.16 and 8.17.
Alternatively, we could implement a less ice intermediate solution that would still support 8.16.
Also note that there is a mention of 8.17 in numbers.v which I didn't handle here.
Note that this requires dropping support for Coq 8.16 and 8.17.
Alternatively, we could implement a less ice intermediate solution that would still support 8.16.
Also note that there is a mention of 8.17 in numbers.v which I didn't handle here.