diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-23 09:39:19 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-23 09:39:19 +0100 |
| commit | d25405f247b2b94527393eba4c79a56291a7fd80 (patch) | |
| tree | c44298d993132140d41a37937eef6e6fc550223b /exportclight | |
| parent | 9c235764664d8aed363b3c2da2d14b9a70ff8094 (diff) | |
| download | compcert-kvx-d25405f247b2b94527393eba4c79a56291a7fd80.tar.gz compcert-kvx-d25405f247b2b94527393eba4c79a56291a7fd80.zip | |
Also refactor clightgen to work with new warnings. Bug 18394
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/ExportClight.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 0e4f1fa3..bce8a9b6 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -400,14 +400,14 @@ let print_variable p (id, v) = let print_globdef p (id, gd) = match gd with - | Gfun(Clight.Internal f) -> print_function p (id, f) - | Gfun(Clight.External _) -> () + | Gfun(Ctypes.Internal f) -> print_function p (id, f) + | Gfun(Ctypes.External _) -> () | Gvar v -> print_variable p (id, v) let print_ident_globdef p = function - | (id, Gfun(Clight.Internal f)) -> + | (id, Gfun(Ctypes.Internal f)) -> fprintf p "(%a, Gfun(Internal f_%s))" ident id (extern_atom id) - | (id, Gfun(Clight.External(ef, targs, tres, cc))) -> + | (id, Gfun(Ctypes.External(ef, targs, tres, cc))) -> fprintf p "@[<hov 2>(%a,@ @[<hov 2>Gfun(External %a@ %a@ %a@ %a))@]@]" ident id external_function ef typlist targs typ tres callconv cc | (id, Gvar v) -> @@ -527,11 +527,11 @@ let name_function f = let name_globdef (id, g) = match g with - | Gfun(Clight.Internal f) -> name_function f + | Gfun(Ctypes.Internal f) -> name_function f | _ -> () let name_program p = - List.iter name_globdef p.Clight.prog_defs + List.iter name_globdef p.Ctypes.prog_defs (* All together *) |