(* * 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.