From 8e5f68c1a6d921a46bb817fe0a82fca1c3494dde Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 7 Jan 2013 10:30:16 +0000
Subject: Update Cminor parser and printer so that the parser can parse the
 whole Cminor language and can reparse the output of the printer.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2090 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/PrintCminor.ml | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

(limited to 'backend/PrintCminor.ml')

diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index dfcabb39..48062759 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -92,16 +92,6 @@ let name_of_binop = function
   | Ocmpu c -> comparison_name c ^ "u"
   | Ocmpf c -> comparison_name c ^ "f"
 
-let name_of_chunk = function
-  | Mint8signed -> "int8signed"
-  | Mint8unsigned -> "int8unsigned"
-  | Mint16signed -> "int16signed"
-  | Mint16unsigned -> "int16unsigned"
-  | Mint32 -> "int32"
-  | Mfloat32 -> "float32"
-  | Mfloat64 -> "float64"
-  | Mfloat64al32 -> "float64al32"
-
 (* Expressions *)
 
 let rec expr p (prec, e) =
@@ -266,8 +256,8 @@ let print_function p id f =
   fprintf p "@;<0 -2>}@]@ "
 
 let print_extfun p id ef =
-  fprintf p "@[<v 0>extern @[<hov 2>\"%s\":@ %a@]@ "
-    (extern_atom id) print_sig (ef_sig ef)
+  fprintf p "@[<v 0>extern @[<hov 2>\"%s\" =@ %s :@ %a@]@ "
+    (extern_atom id) (name_of_external ef) print_sig (ef_sig ef)
 
 let print_init_data p = function
   | Init_int8 i -> fprintf p "int8 %ld" (camlint_of_coqint i)
-- 
cgit