diff options
| -rw-r--r-- | backend/RTLTunnelingproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 14a2c037..51ef0f7a 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -531,7 +531,7 @@ Proof. + eapply exec_Iload_notrap1. * exploit instruction_type_preserved; (simpl; eauto)||congruence. * rewrite <- H1. apply eval_addressing_preserved. apply symbols_preserved. - + apply match_states_intro; try assumption. apply set_reg_lessdef. unfold default_notrap_load_value. apply Val.lessdef_undef. apply RS. + + apply match_states_intro; try assumption. apply set_reg_lessdef. apply Val.lessdef_undef. apply RS. - (* Iload NOTRAP2 *) exploit eval_addressing_lessdef; try eassumption. apply reglist_lessdef; apply RS. |