fact: Definition localVariables (block:t) : list Var := let fix variables (stmts:list STATEMENT.t) : list Var := match stmts with | nil => nil | (Build_statementRec _ _(varDeclStmt v _))::ss => v :: variables ss | _::ss => variables ss end in variables (statements block).
imports: JML(JMLProgramPlus) Coq(ZArith) JML(ZHelpers) JML(LogicHelpers) Coq(Bool) Coq(Sumbool) Coq(Ndec) JML(PosAux) JML(EqBoolAux) Coq(Relation_Operators) Coq(List) JML(ListFunctions) JML(ListHelpers) JML(OptionHelpers)