From 5525293cb8e2cfe371e0f195227918a6726904bd Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 6 Sep 2006 13:10:11 +0000 Subject: MAJ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@79 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- caml/CMparser.mly | 4 +++- caml/PrintPPC.ml | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/caml/CMparser.mly b/caml/CMparser.mly index 5595afed..2df44fb3 100644 --- a/caml/CMparser.mly +++ b/caml/CMparser.mly @@ -148,7 +148,9 @@ global_declarations: global_declaration: VAR STRINGLIT LBRACKET INTLIT RBRACKET - { Coq_pair($2, Coq_cons(Init_space (z_of_camlint $4), Coq_nil)) } + { Coq_pair(Coq_pair($2, + Coq_cons(Init_space (z_of_camlint $4), Coq_nil)), + ()) } ; proc_list: 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 -> () | _ -> -- cgit