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

1 files changed, 1 insertions, 9 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 66c7a3c..c66d6b0 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -412,15 +412,7 @@ Definition transf_function (f: RTL.function) : option LTL.function :=
   end.
 
 Definition transf_fundef (fd: RTL.fundef) : option LTL.fundef :=
-  match fd with
-  | External ef =>
-      if type_external_function ef then Some (External ef) else None
-  | Internal f =>
-      match transf_function f with
-      | None => None
-      | Some tf => Some (Internal tf)
-      end
-  end.
+  transf_partial_fundef transf_function fd.
 
 Definition transf_program (p: RTL.program) : option LTL.program :=
   transform_partial_program transf_fundef p.