diff options
Diffstat (limited to 'mppa_k1c/Asmgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index 7f070c12..8bbdbd4c 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -553,9 +553,9 @@ Lemma transl_cond_int32s_correct: Proof. intros. destruct cmp; simpl. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. + split; intros; Simpl. destruct (rs##r1); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. + split; intros; Simpl. destruct (rs##r1); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. split; intros; Simpl. - econstructor; split. |