search

coq-community / autosubst

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
https://www.ps.uni-saarland.de/autosubst
MIT License
50 stars 14 forks source link

bump compatible Coq version to 8.18~ #32

Closed haselwarter closed 1 year ago

RalfJung commented 1 year ago

Strange, it builds with coq.dev but on 8.17 we get a deprecation error (not warning)?

palmskog commented 1 year ago

@RalfJung they turned the deprecated-instance-without-locality warning into an error in 8.17. All you need to do is add this flag in the right place (which I'm not sure where it is):

-arg -w -arg -deprecated-instance-without-locality
palmskog commented 1 year ago

And the reason it works on Coq master is that it has a new definition of default locality.

RalfJung commented 1 year ago

We should probably add the missing Global everywhere...

RalfJung commented 1 year ago

Thanks!