Module RTLgenproofC
Let SEGETGT: senv_genv_compat skenv_link tge. Proof. eapply SkEnv.senv_genv_compat; et. Qed.
Inductive match_states_at: Cminor.state -> CminorSel.state -> SimMem.t -> SimMem.t -> Prop :=
| match_states_at_intro
fptr sg vs k m st_tgt sm_at sm_arg
(ATEXT: Genv.find_funct ge fptr = None):
match_states_at (Cminor.Callstate fptr sg vs k m) st_tgt sm_at sm_arg.
Theorem sim_modsem: ModSemPair.sim msp.
Proof.
End SIMMODSEM.
Section SIMMOD.
Variable prog: CminorSel.program.
Variable tprog: RTL.program.
Hypothesis TRANSL: match_prog prog tprog.
Definition mp: ModPair.t := ModPair.mk (CminorSelC.module prog) (RTLC.module tprog) tt.
Theorem sim_mod: ModPair.sim mp.
Proof.
End SIMMOD.