search

mit-plv / bbv

Bedrock Bit Vector Library
MIT License
27 stars 23 forks source link

Incompatibility with coq.8.17.1 #46

Open ric-almeida opened 1 year ago

ric-almeida commented 1 year ago

When trying to resintall coq-bbv.1.3 after upgrading coq in opam to 8.17.1, the following error is produced:

File "./src/bbv/DepEq.v", line 17, characters 0-32:
Error: The default value for rewriting hint locality is currently "global"
outside sections, but is scheduled to change to "export" in the next release
(Coq 8.18). In Coq 8.17, not providing an explicit locality outside sections
triggers a fatal warning, to ensure that hint localities are made explicit
before the upcoming change in the default value. It is recommended to use
"export" whenever possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example: "#[export] Hint Rewrite foo
: bar." This is supported since Coq 8.14.
[deprecated-hint-rewrite-without-locality,deprecated]
bacam commented 1 year ago

I think this just needs a new release. I'm happy to do the opam repo wrangling if necessary, but someone here would still have to tag the release.