bbv
bbv copied to clipboard
Incompatibility with coq.8.17.1
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]
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.