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/Machtyping.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'backend/Machtyping.v')

diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index 24f0ddb6..ad3ee886 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -83,7 +83,6 @@ Record wt_function (f: function) : Prop := mk_wt_function {
 
 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