Library compcertx.backend.ValueAnalysisImplX

In this file, we repackage an instance for compcert.backend.ValueDomain.MMatch for the concrete memory model implemented in compcertx.common.MemimplX.
Indeed, those two memory models are different as they use different implementations of inject_neutral.
Fortunately, MMatch does not use inject_neutral, so we have nothing to prove. We just need to unpack/repack.
Not even, thanks to reparameterization of ValueAnalysisImpl.

Require compcert.backend.ValueAnalysisImpl.
Require ValueDomainImplX.

Import Coqlib.
Export ValueAnalysis.
Export MemimplX.
Export ValueAnalysisImpl.