Require  VST.concurrency.common.core_semantics.
Require  VST.sepcomp.mem_lemmas.
Require  VST.sepcomp.structured_injections.
Require  VST.sepcomp.effect_semantics.
Require  VST.sepcomp.extspec.
Require  VST.sepcomp.Address.
Module SepComp.
 Export VST.concurrency.common.core_semantics.
 Export VST.sepcomp.mem_lemmas.
 Export VST.sepcomp.structured_injections.
 Export VST.sepcomp.effect_semantics.
 Export VST.sepcomp.extspec.
 Export VST.sepcomp.Address.
End SepComp.

