diff --git a/caml/CMparser.mly b/caml/CMparser.mly
index 5595afed92bf2e2b5390e6d65d56ca69c2f51e4c..2df44fb33be56aa2cdb28e907a29c091f9e0b430 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 eaa383b4e66fe08de1bcc146b99fbd35b3c3bbeb..790c3e57aaf4a1f722f07516ea9788f925bfec9a 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 -> ()
   | _  ->