Require Export VST.veric.base.
Require Export VST.msl.msl_standard.
Require Export VST.veric.rmaps.

Require Export VST.veric.rmaps_lemmas.

Require Export VST.veric.compcert_rmaps.

(* Module Mem : MEM := compcert.common.Memory.Mem. *)
Export Mem.
Open Scope Z.
