Module Wp.MemVal

module MemVal: sig .. end

module type State = sig .. end
module type Value = sig .. end
module Make: 
functor (V : Value-> Wp.Sigs.Model
module Eva: Value 

The glue between WP and EVA.