(*
 * Copyright (c) 2017-present,
 * Programming Research Laboratory (ROPAS), Seoul National University, Korea
 * This software is distributed under the term of the BSD-3 clause license.
 *)
Set Implicit Arguments.

Require Import Morphisms.
Require Import Monad vgtac DLat DMap DPow DStr DFMapAVL Syn UserInputType Global.
Require DMem.
Require Import DomBasic DomAbs.

Load DomMemCommon.