diff options
Diffstat (limited to 'powerpc/Asmgenproof1.v')
-rw-r--r-- | powerpc/Asmgenproof1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 8c9fd2bd..2e609900 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1262,13 +1262,13 @@ Qed. Lemma transl_select_op_correct: forall cond args ty r1 r2 rd k rs m c, transl_select_op cond args r1 r2 rd k = OK c -> - important_preg r1 = true -> important_preg r2 = true -> + important_preg rd = true -> important_preg r1 = true -> important_preg r2 = true -> exists rs', exec_straight ge fn c rs m k rs' m /\ Val.lessdef (Val.select (eval_condition cond (map rs (map preg_of args)) m) rs#r1 rs#r2 ty) rs'#rd /\ forall r, important_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. - intros until c. intros TR IMP1 IMP2. + intros until c. intros TR IMP1 IMP2 IMP3. unfold transl_select_op in TR. destruct (ireg_eq r1 r2). - inv TR. econstructor; split; [|split]. |