fact: Definition EvalResult (st : State.t) : option Value := match Frame.ret st@fr with | Normal val => val | Exception loc => Some (Ref loc) end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)