From 1fe68ad575178f7d8a775906947d2fed94d40976 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 30 Jul 2011 09:54:35 +0000
Subject: ARM codegen ported to new ABI + VFD floats

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/ConstpropOpproof.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'arm/ConstpropOpproof.v')

diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 25758cc8..4d430822 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -143,6 +143,8 @@ Proof.
 
   inv H4. destruct (Float.intoffloat f); simpl in H0; inv H0. red; auto.
 
+  inv H4. destruct (Float.intuoffloat f); simpl in H0; inv H0. red; auto.
+
   caseEq (eval_static_condition c vl0).
   intros. generalize (eval_static_condition_correct _ _ _ m _ H H1).
   intro. rewrite H2 in H0. 
-- 
cgit