Closed andrew-appel closed 6 months ago
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.
also msl/predicates_hered.v
This seems to have been fixed by #677.
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.