diff options
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 60c11dc..1f2c736 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -871,8 +871,8 @@ Proof. econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. simpl. auto. caseEq (Float.cmp Clt x fm); intros. - rewrite Float.intuoffloat_intoffloat_1 in H0; auto. - EvalOp. simpl. rewrite H0; auto. + exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ. + EvalOp. simpl. rewrite EQ; auto. exploit Float.intuoffloat_intoffloat_2; eauto. intro EQ. replace n with (Int.add (Int.sub n Float.ox8000_0000) Float.ox8000_0000). apply eval_addimm. eapply eval_intoffloat; eauto. |