From 7998ccfd709b97f1a2306df4570365d58a5bb4b5 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 12 Jan 2014 10:48:56 +0000
Subject: - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to
 4. - Revised printing of intermediate RTL code.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 checklink/Check.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'checklink')

diff --git a/checklink/Check.ml b/checklink/Check.ml
index 8e8afd1..6c1739c 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -2493,7 +2493,7 @@ and check_builtin_vload_common ccode ecode pc chunk addr offset res fw =
           >>= recur_simpl
       | _ -> error
       end
-  | (Mfloat64 | Mfloat64al32), [FR res] ->
+  | Mfloat64, [FR res] ->
       begin match ecode with
       | LFD(frD, rA, d) :: es ->
           OK(fw)
@@ -2553,7 +2553,7 @@ and check_builtin_vstore_common ccode ecode pc chunk addr offset src fw =
           >>= compare_code ccode es (Int32.add pc 8l)
       | _ -> error
       end
-  | (Mfloat64 | Mfloat64al32), FR src ->
+  | Mfloat64, FR src ->
       begin match ecode with
       | STFD(frS, rA, d) :: es ->
           OK(fw)
-- 
cgit v1.2.3