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 | |
parent | 14a9bb4b267eeead8cd9503ee19e860a8bc0d763 (diff) | |
download | compcert-e884946c8788db4eb791fa93761d487b9de13ae4.tar.gz compcert-e884946c8788db4eb791fa93761d487b9de13ae4.zip |
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')
-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 60c11dcb..1f2c7362 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. |