From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 4 Aug 2007 07:27:50 +0000
Subject: Fusion des modifications faites sur les branches "tailcalls" et
 "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC
 - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout
 des langages intermediaires CminorSel et LTLin correspondants - Ajout des
 tailcalls depuis Cminor jusqu'a PPC

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 caml/PrintPPC.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'caml/PrintPPC.ml')

diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index 3ee79d12..bf7b2cc7 100644
--- a/caml/PrintPPC.ml
+++ b/caml/PrintPPC.ml
@@ -137,6 +137,8 @@ let print_instruction oc labels = function
       fprintf oc "	bf	%a, %a\n" print_crbit bit print_label lbl
   | Pbl s ->
       fprintf oc "	bl	%a\n" print_symb s
+  | Pbs s ->
+      fprintf oc "	b	%a\n" print_symb s
   | Pblr ->
       fprintf oc "	blr\n"
   | Pbt(bit, lbl) ->
@@ -318,10 +320,6 @@ let print_instruction oc labels = function
       fprintf oc "	xoris	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
   | Plabel lbl ->
       if Labelset.mem lbl labels then fprintf oc "%a:\n" print_label lbl
-  | Piundef r ->
-      fprintf oc "	# undef %a\n" ireg r
-  | Pfundef r ->
-      fprintf oc "	# undef %a\n" freg r
 
 let rec labels_of_code = function
   | Coq_nil -> Labelset.empty
-- 
cgit