Skip to content

Incompatibility with coq.8.17.1 #46

Description

@ric-almeida

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]

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions