diff options
Diffstat (limited to 'backend/RTLTunnelingproof.v')
| -rw-r--r-- | backend/RTLTunnelingproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 2cef08e2..aa21fc06 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -461,7 +461,7 @@ Proof. left. eexists. split. * eapply exec_Iload. -- exploit instruction_type_preserved; (simpl; eauto)||congruence. - -- eapply has_loaded_normal; eauto. rewrite <- EVAL'. apply eval_addressing_preserved. apply symbols_preserved. + -- try (eapply has_loaded_normal; eauto; rewrite <- EVAL'; apply eval_addressing_preserved; apply symbols_preserved). * apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS. + destruct (eval_addressing) eqn:EVAL in LOAD. * specialize (LOAD v). @@ -473,7 +473,7 @@ Proof. -- left; eexists; split. eapply exec_Iload. ++ exploit instruction_type_preserved; (simpl; eauto)||congruence. - ++ eapply has_loaded_normal; eauto. rewrite <- ADDR. apply eval_addressing_preserved. apply symbols_preserved. + ++ try (eapply has_loaded_normal; eauto; rewrite <- ADDR; apply eval_addressing_preserved; apply symbols_preserved). ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto. -- left; eexists; split. eapply exec_Iload. |