From 210352d90e5972aabfb253f7c8a38349f53917b3 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 22 Oct 2006 16:54:24 +0000
Subject: Lever la restriction sur les fonctions externes, restriction qui
 exigeait que tous les arguments resident en registres

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Lineartyping.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'backend/Lineartyping.v')

diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 3a0ee13..cbe1831 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -254,7 +254,6 @@ Definition wt_function (f: function) : Prop :=
 
 Inductive wt_fundef: fundef -> Prop :=
   | wt_fundef_external: forall ef,
-      Conventions.sig_external_ok ef.(ef_sig) ->
       wt_fundef (External ef)
   | wt_function_internal: forall f,
       wt_function f ->
-- 
cgit v1.2.3