diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-01-15 10:30:11 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-01-15 10:30:11 +0100 |
| commit | 2b598161e216402db6fe3780f1a00d7802bccb21 (patch) | |
| tree | b18318515d71829ad0081b1ee1e07d0895736caa /exportclight | |
| parent | ce7013f94c97b0e46da03c97812b38df001fbc9d (diff) | |
| download | compcert-kvx-2b598161e216402db6fe3780f1a00d7802bccb21.tar.gz compcert-kvx-2b598161e216402db6fe3780f1a00d7802bccb21.zip | |
Added type annotations for exported program. (#50)v3.2
Added types for global_definitions in order to avoid problems with
implicit parameters. This should fix issue 215
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/ExportClight.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 6f5e3cdc..1b1402c3 100644 --- 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 := @ "; |