From b7e0d70de2ace6f0a22f9f65cc244d875ee48496 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sat, 1 Jun 2019 08:48:20 +0200
Subject: ARM: select is not supported at type Tlong

---
 arm/SelectOpproof.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'arm/SelectOpproof.v')

diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index f281f7ce..8b546971 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -746,7 +746,9 @@ Theorem eval_select:
      eval_expr ge sp e m le a v
   /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
 Proof.
-  unfold select; intros; inv H. rewrite <- H3; TrivialExists. 
+  unfold select; intros.
+  destruct (match ty with Tint | Tfloat | Tsingle => true | _ => false end); inv H.
+  rewrite <- H3; TrivialExists. 
 Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
-- 
cgit