From e884946c8788db4eb791fa93761d487b9de13ae4 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 29 Oct 2010 14:21:59 +0000 Subject: float->int conversions, continued: weaker axiomatization. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1545 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/SelectOpproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/SelectOpproof.v') diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 87dc63ee..cdb21cbe 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -953,8 +953,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. -- cgit