From 14f375f7b879d9ccfb06845b2dbe1a907851e330 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 12 Jan 2014 12:41:08 +0000
Subject: Eradication of Mfloat64al32, continued.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2404 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/SelectOp.vp | 2 --
 1 file changed, 2 deletions(-)

(limited to 'arm/SelectOp.vp')

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 767e7471..2b0bdff8 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -401,7 +401,6 @@ Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
   | Mint64 => false
   | Mfloat32 => false
   | Mfloat64 => false
-  | Mfloat64al32 => false
   end.
 
 Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
@@ -414,7 +413,6 @@ Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
   | Mint64 => false
   | Mfloat32 => false
   | Mfloat64 => false
-  | Mfloat64al32 => false
   end.
 
 Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
-- 
cgit