future-coercion-class-field warning

[andrew-appel]

In veric/ghosts.v, floyd/printf.v, and in some other files in msl/, veric/, floyd/, there are Class declarations that are newly marked as deprecated in Coq 8.17, and will stop working sometime in the future. Below is an example of the message. I'm not sure what's the best way to fix this, especially in a way that stays compatible with Coq 8.16.

File "./veric/ghosts.v", line 174, characters 0-275:
Warning: A coercion will be introduced instead of an instance in future
versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or
use '#[global] Existing Instance field.' for compatibility with Coq < 8.17).
Beware that the default locality for '::' is #[export], as opposed to
#[global] for ':>' currently. Add an explicit #[global] attribute to the
field if you need to keep the current behavior. For example: "Class foo := {
#[global] field :: bar }." [future-coercion-class-field,records]

[mansky1]

Oh, interesting! I'll try a few approaches. I also noticed that they've finally included "Disable Notation", which might help with some of the map notation clashes.

[andrew-appel]

also msl/predicates_hered.v

[andrew-appel]

This seems to have been fixed by #677.