Coq-HoTT
Coq-HoTT copied to clipboard
remove 8.15 compat
We had some compat code leftover.
Does this mean it won't build with 8.15 anymore? Maybe we should keep compatibility until we have a strong reason to not be compatible, as some users might not have upgraded to 8.16.
@jdchristensen Yes. We were compatible with 8.16 for a while. #1661 was meant to bump our least supported version to 8.16 (perhaps I didn't make that clear enough).
The reason being is that there are some 8.16 features I would like to start using. This isn't essential but perhaps I miscommunicated my last PR.
Well, even after #1661, the library should still be usable with 8.15. I would prefer to delay removing the compatibility code until we have merged something else that prevents the library from being used with 8.15. 8.16 was only released a week ago...
@jdchristensen As you wish, this PR does no harm sitting here.
@jdchristensen Since #1697 is going to use 8.16 features, I think we should merge this.
I agree. LGTM.