diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-10-29 14:21:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-10-29 14:21:59 +0000 |
| commit | e884946c8788db4eb791fa93761d487b9de13ae4 (patch) | |
| tree | ab259b25d2ebdf70278314160374dbbbe79e8901 /powerpc/SelectOpproof.v | |
| parent | 14a9bb4b267eeead8cd9503ee19e860a8bc0d763 (diff) | |
float->int conversions, continued: weaker axiomatization.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1545 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
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. |