aboutsummaryrefslogtreecommitdiffstats
path: root/caml/PrintPPC.ml
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-06 13:10:11 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-06 13:10:11 +0000
commit5525293cb8e2cfe371e0f195227918a6726904bd (patch)
treedbafee85ed2523540b2fdd29e678442ec584f617 /caml/PrintPPC.ml
parentabf06dadb072b3b8eb0488ce1c72b22bd802b116 (diff)
downloadcompcert-5525293cb8e2cfe371e0f195227918a6726904bd.tar.gz
compcert-5525293cb8e2cfe371e0f195227918a6726904bd.zip
MAJ
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@79 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml/PrintPPC.ml')
-rw-r--r--caml/PrintPPC.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index eaa383b4..790c3e57 100644
--- a/caml/PrintPPC.ml
+++ b/caml/PrintPPC.ml
@@ -374,7 +374,7 @@ let print_init_data oc = function
let n = camlint_of_z n in
if n > 0l then fprintf oc " .space %ld\n" n
-let print_var oc (Coq_pair(name, init_data)) =
+let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
match init_data with
| Coq_nil -> ()
| _ ->