Coq 8.14 warnings
New warnings in Coq 8.14 are triggered both by .v files produced by Menhir, and by .v files from the Coq library coq-menhirlib.
Concerning the latter, here is a fix: https://github.com/AbsInt/CompCert/pull/415/commits/05514d7ef81dda3cbfa3cf5fe3f12d892fc1477f
I elected to use Global Instance
instead of [#export] Instance
because the latter is not supported before Coq 8.13.
Concerning Menhir-generated Coq files: Instance
needs to be qualified as Global Instance
, for the same reasons.