diff options
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 3fbc9912..5dd5ee04 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -63,7 +63,7 @@ Proof. destruct rel as [rel | ]; simpl; intros. 2: contradiction. eapply forward_move_sound; eauto. - Qed. +Qed. Lemma forward_move_l_b_sound : forall rel rs m x, @@ -447,7 +447,6 @@ Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. -Proof. induction 1; intros S1' MS; inv MS. - (* Inop *) exists (State ts tf sp pc' rs m). split. |