Merge branch 'master' of github.com:AbsInt/CompCert

1 files changed, 9 insertions, 3 deletions

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index f5b8150d..1b1402c3 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -109,6 +109,12 @@ let coqint p n =
   then fprintf p "(Int.repr %ld)" n
   else fprintf p "(Int.repr (%ld))" n
 
+let coqptrofs p n =
+  let s = Z.to_string n in
+  if Z.ge n Z.zero
+  then fprintf p "(Ptrofs.repr %s)" s
+  else fprintf p "(Ptrofs.repr (%s))" s
+
 let coqint64 p n =
   let n = camlint64_of_coqint n in
   if n >= 0L
@@ -393,7 +399,7 @@ let init_data p = function
   | Init_float32 n -> fprintf p "Init_float32 %a" coqsingle n
   | Init_float64 n -> fprintf p "Init_float64 %a" coqfloat n
   | Init_space n -> fprintf p "Init_space %ld" (Z.to_int32 n)
-  | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqint ofs
+  | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqptrofs ofs
 
 let print_variable p (id, v) =
   fprintf p "Definition v_%s := {|@ " (extern_atom id);
@@ -549,10 +555,10 @@ let print_program p prog =
   fprintf p "Definition composites : list composite_definition :=@ ";
   print_list print_composite_definition p prog.prog_types;
   fprintf p ".@ @ ";
-  fprintf p "Definition global_definitions :=@ ";
+  fprintf p "Definition global_definitions : list (ident * globdef fundef type) :=@ ";
   print_list print_ident_globdef p prog.Ctypes.prog_defs;
   fprintf p ".@ @ ";
-  fprintf p "Definition public_idents :=@ ";
+  fprintf p "Definition public_idents : list ident :=@ ";
   print_list ident p prog.Ctypes.prog_public;
   fprintf p ".@ @ ";
   fprintf p "Definition prog : Clight.program := @ ";