diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-29 15:54:41 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-29 15:54:41 +0100 |
| commit | 4d79ef052cc05240d6613bb22ef1ec547b17d3e1 (patch) | |
| tree | 8caa2cda1f8ae914a27e7ad313283c5a166f3708 /backend/CSE3proof.v | |
| parent | 47fb65a38064a29729d103e51393dde156239917 (diff) | |
| download | compcert-kvx-4d79ef052cc05240d6613bb22ef1ec547b17d3e1.tar.gz compcert-kvx-4d79ef052cc05240d6613bb22ef1ec547b17d3e1.zip | |
in CSE3 choose lowest variable as representative for moves
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. |