In the CompCert trunk, it appears that meminj_preserves_globals has been moved from common.Events to backend.Unusedglobproof.
But VST does use this lemma. Please move it back to Events. I suppose I could copy-paste it into VST, but that would perhaps be more fragile.
See also:
https://gitlab.inria.fr/coq/coq/-/jobs/7902971
In the CompCert trunk, it appears that meminj_preserves_globals has been moved from common.Events to backend.Unusedglobproof.
But VST does use this lemma. Please move it back to Events. I suppose I could copy-paste it into VST, but that would perhaps be more fragile.
See also:
https://gitlab.inria.fr/coq/coq/-/jobs/7902971