Added type annotations for exported program. (#50)

Added types for global_definitions in order to avoid problems with implicit parameters. This should fix issue 215
AbsInt · Jan 15, 2018 · 2b59816 · 2b59816
1 parent ce7013f
commit 2b59816
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
@@ -555,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 := @ ";