From 33b742bb41725e47bd88dc12f2a4f40173023f83 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 27 Mar 2015 14:24:03 +0100
Subject: Updated the Caml part.  Added some more tests in annot1.c.

---
 backend/PrintMach.ml | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

(limited to 'backend/PrintMach.ml')

diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index b356ca9e..8484a5c3 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -34,15 +34,6 @@ let rec regs pp = function
   | [r] -> reg pp r
   | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
 
-let annot_param pp = function
-  | APreg r -> reg pp r
-  | APstack(chunk, ofs) -> fprintf pp "stack(%s,%ld)" (name_of_chunk chunk) (camlint_of_coqint ofs)
-
-let rec annot_params pp = function
-  | [] -> ()
-  | [r] -> annot_param pp r
-  | r1::rl -> fprintf pp "%a, %a" annot_param r1 annot_params rl
-
 let ros pp = function
   | Coq_inl r -> reg pp r
   | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
@@ -78,7 +69,8 @@ let print_instruction pp i =
       fprintf pp "\t%a = %s(%a)\n"
         regs res (name_of_external ef) regs args
   | Mannot(ef, args) ->
-      fprintf pp "\t%s(%a)\n" (name_of_external ef) annot_params args
+      fprintf pp "\t%s(%a)\n"
+        (name_of_external ef) (print_annot_args reg) args
   | Mlabel lbl ->
       fprintf pp "%5d:" (P.to_int lbl)
   | Mgoto lbl ->
-- 
cgit