Coq-HoTT icon indicating copy to clipboard operation
Coq-HoTT copied to clipboard

Published 20 hours ago • verified publisher icon HoTT

remove 8.15 compat

Open Alizter opened this issue 1 year ago • 4 comments

We had some compat code leftover.

Alizter avatar Sep 13 '22 16:09 Alizter

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 avatar Sep 13 '22 17:09 jdchristensen

@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.

Alizter avatar Sep 13 '22 17:09 Alizter

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 avatar Sep 13 '22 18:09 jdchristensen

@jdchristensen As you wish, this PR does no harm sitting here.

Alizter avatar Sep 13 '22 18:09 Alizter

@jdchristensen Since #1697 is going to use 8.16 features, I think we should merge this.

Alizter avatar Jan 21 '23 17:01 Alizter

I agree. LGTM.

jdchristensen avatar Jan 21 '23 17:01 jdchristensen