fact: Definition f_main := {| fn_return := tint; fn_callconv := cc_default; fn_params := nil; fn_vars := nil; fn_temps := nil; fn_body := (Ssequence (Sreturn (Some (Econst_int (Int.repr 0) tint))) (Sreturn (Some (Econst_int (Int.repr 0) tint)))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)